Universes for discrimination proofs

I can't decide if this is trivial or not. What does this construction mean/say?

module Universe where

data N0 : Set where

data Bool : Set where
 True : Bool
 False : Bool

data Direction : Set where
 Left : Direction
 Right : Direction

data Eq (T : Set) : T -> T -> Set where
 refl : (t : T) -> Eq T t t

-- Eq Set Bool Direction -> N0
--  is not provable
--  (techincally I would have to define Eq in Set1 but we can pretend universe polymorphism)

mutual
 data U : Set where
  n0 : U
  bool : U
  direction : U
  eq : (A : U) -> T A -> T A -> U
  pi : (A : U) -> (B : T A -> U) -> U
 
 T : U -> Set
 T n0 = N0
 T bool = Bool
 T direction = Direction
 T (eq A x y) = Eq (T A) x y
 T (pi A B) = (a : T A) -> T (B a)

mutual
 data U1 : Set where
  n0' : U1
  bool' : U1
  direction' : U1
  eq' : (A : U1) -> T1 A -> T1 A -> U1
  pi' : (A : U1) -> (B : T1 A -> U1) -> U1
  u' : U1
  lift : U -> U1
 
 T1 : U1 -> Set
 T1 n0' = N0
 T1 bool' = Bool
 T1 direction' = Direction
 T1 (eq' A x y) = Eq (T1 A) x y
 T1 (pi' A B) = (a : T1 A) -> T1 (B a)
 T1 u' = U
 T1 (lift A) = T A

T' : U -> Set
T' n0 = T n0
T' bool = T bool
T' direction = T n0
T' (eq A x y) = T n0
T' (pi A B) = T n0

rew : forall {A B : U} -> Eq U A B -> T' A -> T' B
rew (refl _) prf = prf

discr : Eq U bool direction -> N0
discr prf = rew prf True

corr : T1 (pi' (eq' u' bool direction) \_ -> n0')
corr = discr

A different approach

Just typing out stuff from http://www.cs.nott.ac.uk/~pwm/ .

module Universe where

open import Data.Nat

data SPT : ℕ -> Set1 where
 vz : {n : ℕ} -> SPT (suc n)
 vs : {n : ℕ} -> SPT n -> SPT (suc n)
 _[_] : {n : ℕ} -> SPT (suc n) -> SPT n -> SPT n
 “0” : {n : ℕ} -> SPT n
 “1” : {n : ℕ} -> SPT n
 _“+”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
 _“×”_ : {n : ℕ} -> SPT n -> SPT n -> SPT n
 _“->”_ : {n : ℕ} -> (K : Set) -> SPT n -> SPT n
 “μ”_ : {n : ℕ} -> SPT (suc n) -> SPT n

data Tel : ℕ -> (ℕ -> Set1) -> Set2 where
 ε : (F : ℕ -> Set1) -> Tel zero F
 _^_ : {F : ℕ -> Set1} -> {n : ℕ} -> F n -> Tel n F -> Tel (suc n) F

data ⟦_⟧_ : {n : ℕ} -> SPT n -> Tel n SPT -> Set2 where
 top : {n : ℕ} -> {T' : Tel n SPT} -> {T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ vz ⟧ (T ^ T')
 pop : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ vs T ⟧ (S ^ T')
 def : {n : ℕ} -> {T' : Tel n SPT} -> {A : SPT n} -> {F : SPT (suc n)} ->
   ⟦ F ⟧ (A ^ T') -> ⟦  F [ A ]  ⟧ T'
 void : {n : ℕ} -> {T' : Tel n SPT} ->
   ⟦ “1” ⟧ T'
 inl : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ S ⟧ T' -> ⟦ S “+” T ⟧ T'
 inr : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ T ⟧ T' -> ⟦ S “+” T ⟧ T'
 pair : {n : ℕ} -> {T' : Tel n SPT} -> {S T : SPT n} ->
   ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ S “×” T ⟧ T'
 funk : {n : ℕ} -> {T' : Tel n SPT} -> {K : Set} -> {T : SPT n} ->
  (f : K -> ⟦ T ⟧ T') -> ⟦ (K “->” T) ⟧ T'
 miso : {n : ℕ} -> {T' : Tel n SPT} -> {F : SPT (suc n)} ->
   ⟦ F ⟧ ((“μ” F) ^ T') -> ⟦ (“μ” F) ⟧ T'



“Nat” : {n : ℕ} -> SPT n
“Nat” = “μ” (“1” “+” vz)

“zero” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T'
“zero” = miso (inl (void))

“succ” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“succ” x = miso (inr (top x))


data “Nat”-View : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> Set2 where
 isZero : {n : ℕ} -> {T' : Tel n SPT} -> “Nat”-View {n} {T'} “zero”
 isSucc : {n : ℕ} -> {T' : Tel n SPT} -> (x : ⟦ “Nat” ⟧ T') -> “Nat”-View {n} {T'} (“succ” x)

viewNat : {n : ℕ} -> {T' : Tel n SPT} -> (n : ⟦ “Nat” ⟧ T') -> “Nat”-View n
viewNat {n} {T'} (miso Q) = aux1 Q
 where aux3 : (r : ⟦ vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inr r))
       aux3 (top x) = isSucc x
       aux2 : (l : ⟦ “1” ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso (inl l))
       aux2 void = isZero
       aux1 : (u : ⟦ “1” “+” vz ⟧ ((“μ” (“1” “+” vz)) ^ T')) -> “Nat”-View (miso u)
       aux1 (inl U) = aux2 U
       aux1 (inr V) = aux3 V

“add” : {n : ℕ} -> {T' : Tel n SPT} -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T' -> ⟦ “Nat” ⟧ T'
“add” x y with viewNat x
“add” (miso (inl (void))) y | isZero = y
“add” (miso (inr (top x))) y | isSucc .x = “succ” (“add” x y)


test = “add” {zero} {ε SPT}
         (“succ” (“succ” (“succ” “zero”)))
         (“succ” (“succ” “zero”))

{- =
miso
(inr
 (top
  (miso
   (inr
    (top
     (miso
      (inr
       (top
        (miso (inr (top (miso (inr (top (miso (inl void)))))))))))))))) -}

Emulate Agda style pattern matching in Coq using ideas frow Eliminating Dependent Pattern Matching..

Require Import JMeq.
Infix "==" := JMeq (at level 31).
Notation "[ x : X ]  == [ y : Y ]" := (@JMeq X x Y y) (at level 30).
Notation "X =/= Y" := (JMeq _ X _ Y -> False) (at level 30).


Derive NoConfusion nat.
Definition noConfusion_nat (P : Type) (u v : nat) : JMeq u v -> NoConfusion_nat P u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.


Inductive SPT : nat -> Type :=
| vz {n} : SPT (S n)
| vs {n} : SPT n -> SPT (S n)
| of {n} : SPT (S n) -> SPT n -> SPT n
| q_zero_q {n} : SPT n
| q_one_q {n} : SPT n
| q_sum_q {n} : SPT n -> SPT n -> SPT n
| q_mul_q {n} : SPT n -> SPT n -> SPT n
| q_arrow_q {n} : Type -> SPT n -> SPT n
| q_mu_q {n} : SPT (S n) -> SPT n.
Derive NoConfusion SPT.
Definition noConfusion_SPT (P : Type) (e1 : nat) (u v : SPT e1) : JMeq u v -> NoConfusion_SPT P e1 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Inductive Tel : nat -> (nat -> Type) -> Type :=
| eps : forall {F}, Tel 0 F
| telCons : forall {F} {n}, Tel n F -> F n -> Tel (S n) F.
Infix ";" := telCons (at level 27, left associativity).
Derive NoConfusion Tel.
Definition noConfusion_Tel (P : Type) (e1 : nat) (e2 : nat -> Type) (u v : Tel e1 e2) : JMeq u v -> NoConfusion_Tel P e1 e2 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Reserved Notation "⟦  type ⟧ scope" (at level 30, no associativity).
Inductive Interpretation : forall n, SPT n -> Tel n SPT -> Type :=
| top {n} {T' : Tel n SPT} {T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ vz ⟧ (T';T)
| pop {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ vs T ⟧ (T';S)
| def {n} {T' : Tel n SPT} {A : SPT n} {F : SPT (S n)}
  : ⟦ F ⟧ (T'; A) -> ⟦ of F A ⟧ T'
| void {n} {T' : Tel n SPT}
  : ⟦ q_one_q ⟧ T'
| inl {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ S ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| inr {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ T ⟧ T' -> ⟦ q_sum_q S T ⟧ T'
| pair {n} {T' : Tel n SPT} {S T : SPT n}
  : ⟦ S ⟧ T' -> ⟦ T ⟧ T' -> ⟦ q_mul_q S T ⟧ T'
| funk {n} {T' : Tel n SPT} {K : Type} {T : SPT n}
  : (K -> ⟦ T ⟧ T') -> ⟦ q_arrow_q K T ⟧ T'
| miso {n} {T' : Tel n SPT} {F : SPT (S n)}
  : ⟦ F ⟧ (T';q_mu_q F) -> ⟦ q_mu_q F ⟧ T'
where "⟦  type ⟧ scope" := (Interpretation _ type scope).
Derive NoConfusion Interpretation.
Definition noConfusion_Interpretation (P : Type) (e1 : nat) (e2 : SPT e1) (e3 : Tel e1 SPT) (u v : ⟦e2 ⟧ e3) : JMeq u v -> NoConfusion_Interpretation P e1 e2 e3 u v.
intros.
elim H.
elim u;
  simpl; intros; tauto.
Defined.



Definition mu_injective (P : Type) (e1 : nat) (u v : SPT (S e1))
  : (e1 == e1 -> u == v -> P) -> (q_mu_q u == q_mu_q v -> P)
  := fun m Eq =>
    noConfusion_SPT P _ (q_mu_q u) (q_mu_q v) Eq m.

Definition mu_vz_clash (P : Type) (n : nat) (F : SPT (S (S n)))
  : q_mu_q F == vz -> P
  := fun Eq =>
    noConfusion_SPT P (S n) (q_mu_q F) vz Eq.



Definition q_Nat_q {n} : SPT n := q_mu_q (q_sum_q q_one_q vz).
Definition q_O_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' := miso (inl void).
Definition q_S_q {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> ⟦ q_Nat_q ⟧ T' := fun x => miso (inr (top x)).

Inductive q_Nat_q'View {n} {T' : Tel n SPT} : ⟦ q_Nat_q ⟧ T' -> Type :=
| isO : q_Nat_q'View q_O_q
| isS : forall x : ⟦ q_Nat_q ⟧ T', q_Nat_q'View (q_S_q x).



Ltac dpm_lift := repeat match goal with H : _ |- _ => intro Eq; revert H; revert Eq end.
Ltac dpm_prepare :=
  match goal with
    | |- @JMeq _ ?x _ ?x -> _ => intros _; dpm_prepare
    | |- @JMeq _ _ _ _ -> _ => dpm_lift
    | _ => intro; dpm_prepare
  end.

Ltac dpm_subst := intro Eql;
  match type of Eql with @JMeq _ ?x _ ?y =>
    (rewrite Eql; clear x Eql) || (rewrite <- Eql; clear y Eql)
  end.

Ltac dpm_confusion := intro Eql;
  match goal with |- ?P =>
    apply (noConfusion_nat P _ _ Eql)||
    apply (noConfusion_SPT P _ _ _ Eql)||
    apply (noConfusion_Tel P _ _ _ _ Eql)||
    apply (noConfusion_Interpretation P _ _ _ _ _ Eql)
  end.

Ltac dpm_specialize := repeat (dpm_prepare; (dpm_subst||dpm_confusion)).



Definition view'q_Nat_q
  (n : nat) (Ts : Tel n SPT) (x : ⟦ q_Nat_q ⟧ Ts) : (@q_Nat_q'View n Ts x).
intros.

refine
  (Interpretation_rect
    (fun n' S' Ts' x' =>
      n == n' -> @q_Nat_q n == S' -> Ts == Ts' -> x == x' ->
      q_Nat_q'View x)
    _ _ _ _ _ _ _ _ _
               n               q_Nat_q                Ts             x
    (JMeq_refl n) (JMeq_refl (@q_Nat_q n)) (JMeq_refl Ts) (JMeq_refl x));
unfold q_Nat_q in *;
dpm_specialize;
intros _.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i' =>
      S n0 == n0' -> q_sum_q q_one_q vz == S' -> T'; q_mu_q (q_sum_q q_one_q vz) == Ts' -> i == i' ->
      q_Nat_q'View (miso i))
    _ _ _ _ _ _ _ _ _
    (S n0) (q_sum_q q_one_q vz) (T'; q_mu_q (q_sum_q q_one_q vz)) i
    (JMeq_refl (S n0)) (JMeq_refl (q_sum_q q_one_q vz)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i));
dpm_specialize;
intros _.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i0' =>
      S n0 == n0' -> q_one_q == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
      q_Nat_q'View (miso (inl i0)))
    _ _ _ _ _ _ _ _ _
    (S n0) q_one_q (T'; q_mu_q (q_sum_q q_one_q vz)) i0
    (JMeq_refl (S n0)) (JMeq_refl (q_one_q)) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize.

exact isO.

refine
  (Interpretation_rect
    (fun n0' S' Ts' i0' =>
      S n0 == n0' -> vz == S' -> (T'; q_mu_q (q_sum_q q_one_q vz)) == Ts' -> i0 == i0' ->
      q_Nat_q'View (miso (inr i0)))
    _ _ _ _ _ _ _ _ _
    (S n0) vz (T'; q_mu_q (q_sum_q q_one_q vz)) i0
    (JMeq_refl (S n0)) (JMeq_refl vz) (JMeq_refl (T'; q_mu_q (q_sum_q q_one_q vz))) (JMeq_refl i0));
dpm_specialize;
intros _.

exact (isS i).

Defined.

Proof of the foldl, foldr relation

-- This is a self contained development of the proof that
--  foldr f z (reverse xs) ≡ foldl (flip f) z xs

-- I use some definitions from
-- http://code.haskell.org/~dolio/agda-play/
-- Particularly Data.List and Relation.Equivality

module Folding where

flip : forall {A B C} -> (A -> B -> C) -> B -> A -> C
flip f b a = f a b


infix  20 _≡_
infixr 30 _≡→_
infixr 25 _lhs_ _rhs_

data _≡_ {a : Set} : a -> a -> Set where
  refl : forall {x} -> x ≡ x

≡sub : forall {a}{P : a -> Set}{x y : a} -> x ≡ y -> P x -> P y
≡sub refl Px = Px

≡symm : forall {a}{x y : a} -> x ≡ y -> y ≡ x
≡symm refl = refl

≡trans : forall {a}{x y z : a} -> x ≡ y -> y ≡ z -> x ≡ z
≡trans refl refl = refl

-- take and equation and apply a function to both sides
_≡→_ : forall {a b}{x y : a} -> x ≡ y -> (f : a -> b) -> f x ≡ f y
refl ≡→ _ = refl

-- rewrite on the left
_lhs_ : forall {a}{x y k : a} -> x ≡ k -> x ≡ y -> y ≡ k
E₁ lhs E₂ = ≡trans (≡symm E₂) E₁

-- rewrite on the right
_rhs_ : forall {a}{x y k : a} -> k ≡ x -> x ≡ y -> k ≡ y
E₁ rhs E₂ = ≡symm (≡symm E₁ lhs E₂)


infixr 50 _∷_ 
infixr 40 _++_

data [_] (a : Set) : Set where
  [] : [ a ]
  _∷_ : a -> [ a ] -> [ a ]


foldr : {a b : Set} -> (a -> b -> b) -> b -> [ a ] -> b
foldr _ z []       = z
foldr f z (a ∷ as) = f a (foldr f z as)

foldl : {a b : Set} -> (b -> a -> b) -> b -> [ a ] -> b
foldl _ z []       = z
foldl f z (a ∷ as) = foldl f (f z a) as

_++_ : forall {a} -> [ a ] -> [ a ] -> [ a ]
[]       ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)

reverse : {A : Set} -> [ A ] -> [ A ]
reverse []       = []
reverse (x ∷ xs) = reverse xs ++ (x ∷ [])


-- Some theorems about ++

-- [] is the right unit
++unit : forall {a} -> (x : [ a ]) -> x ++ [] ≡ x
++unit []       = refl
++unit (x ∷ xs) = ++unit xs ≡→ \s -> x ∷ s

-- Associative
++assoc : forall {a} -> (a b c : [ a ]) ->
   (a ++ b) ++ c ≡ a ++ (b ++ c)
++assoc {_} []       _ _ = refl
++assoc {_} (x ∷ xs) _ _ = ++assoc xs _ _ ≡→ \s -> x ∷ s

++reverse : forall {a} (x y : [ a ]) ->
   reverse y ++ reverse x ≡ reverse (x ++ y)
++reverse [] ys       = ++unit (reverse ys)
++reverse (x ∷ xs) ys = ++reverse xs ys
                        ≡→ (\s -> s ++ reverse (x ∷ []))
                        lhs ++assoc (reverse ys) _ _

++foldr : forall {a b} ->
          (f : a -> b -> b) -> (z : b) -> (xs ys : [ a ]) ->
   foldr f z (xs ++ ys) ≡ foldr f (foldr f z ys) xs
++foldr f z []       ys = refl
++foldr f z (x ∷ xs) ys = ++foldr f z xs ys ≡→ f x

-- This identity is not actually used but I leave it in for
-- the sake of completeness
++foldl : forall {a b} ->
          (f : b -> a -> b) -> (z : b) -> (xs ys : [ a ]) ->
   foldl f z (xs ++ ys) ≡ foldl f (foldl f z xs) ys
++foldl f z []       ys = refl
++foldl f z (x ∷ xs) ys = ++foldl f (f z x) xs ys


foldl^foldr : forall {a b} ->
              (f : a -> b -> b) -> (z : b) -> (xs : [ a ]) ->
   foldr f z (reverse xs) ≡ foldl (flip f) z xs
foldl^foldr f z []       = refl
foldl^foldr f z (x ∷ xs) = foldl^foldr f (f x z) xs
                           lhs ≡symm (++foldr f z
                                              (reverse xs)
                                              (x ∷ []))