Commit 0c531557 authored by Gaspard FEREY's avatar Gaspard FEREY

Added new models for Coq / CiC.

parent 80e6ef1d
#NAME Coq.
(; Natural numbers ;)
Nat : Type.
z : Nat.
s : Nat -> Nat.
def max : Nat -> Nat -> Nat.
[i] max i z --> i.
[j] max z (s j) --> s j.
[i,j] max (s i) (s j) --> s (max i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
set : Sort.
type : Nat -> Sort.
def axiom : Sort -> Sort.
[] axiom prop --> axiom set.
[] axiom set --> type z.
[i] axiom (type i) --> type (s i).
def rule : Sort -> Sort -> Sort.
[] rule prop set --> set.
[s1] rule s1 prop --> prop.
[] rule set set --> set.
[i] rule set (type i) --> type i.
[i] rule (type i) set --> type i.
[i,j] rule (type i) (type j) --> type (max i j).
def sup : Sort -> Sort -> Sort.
[] sup prop prop --> prop.
[] sup set set --> set.
[] sup prop set --> type z. (; ;)
[] sup set prop --> type z.
[i] sup set (type i) --> type i.
[i] sup prop (type i) --> type i.
[i] sup (type i) set --> type i.
[i] sup (type i) prop --> type i.
[i,j] sup (type i) (type j) --> type (max i j).
(; Canonicity rules ;)
[s1] sup s1 s1 --> s1.
[s1,s2] axiom (sup s1 s2) --> sup (axiom s1) (axiom s2).
[s1,s2,s3] sup (sup s1 s2) s3 --> sup s1 (sup s2 s3).
[s1,s2,s3] rule s1 (sup s2 s3) --> sup (rule s1 s2) (rule s1 s3).
[s1,s2,s3] rule (sup s1 s2) s3 --> sup (rule s1 s3) (rule s2 s3).
(; /!\ Confluence broken: the term
(rule (sup s1 s2) (sup s3 s4)) reduces to both
sup (rule s1 s3) (sup (rule s1 s4) (sup (rule s2 s3) (rule s2 s4)))
and
sup (rule s1 s3) (sup (rule s2 s3) (sup (rule s1 s4) (rule s2 s4)))
;)
(; Terms ;)
U : s1 : Sort -> Type.
def T : s1 : Sort -> a : U s1 -> Type.
sort : s1 : Sort -> U (axiom s1).
def lift : s1 : Sort -> s2 : Sort -> U s1 -> U (sup s1 s2).
def prod : s1 : Sort -> s2 : Sort -> a : U s1 -> (T s1 a -> U s2) -> U (rule s1 s2).
[s1]
T _ (sort s1)
--> U s1.
[s1,a]
T _ (lift s1 _ a)
--> T s1 a.
[s1,s2,a,b]
T _ (prod s1 s2 a b)
--> x : T s1 a -> T s2 (b x).
(; Canonicity rules ;)
[s1,a]
lift s1 s1 a
--> a.
[s1,s2,s3,a]
lift _ s3 (lift s1 s2 a)
--> lift s1 (sup s2 s3) a.
[s1,s2,s3,a,b]
prod _ s2 (lift s1 s3 a) (x => b x)
--> lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a (x => b x)).
[s1,s2,s3,a,b]
prod s1 _ a (x => lift s2 s3 (b x))
--> lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
(; Cast ;)
def join : s1 : Sort -> s2 : Sort -> U s1 -> U s2 -> U (sup s1 s2).
[i]
join _ _ i i
--> i.
[s1,s2]
join _ _ (sort s1) (sort s2)
--> sort (sup s1 s2).
(;[s1 : Sort, s2 : Sort, s3 : Sort, s4 : Sort, a : U s1, b : U s3];)
(; join {sup s1 s2} {sup s3 s4} (lift s1 s2 a) (lift s3 s4 b);)
(;--> lift (sup s1 s3) (sup s2 s4) (join s1 s3 a b).;)
[s1,s2,s3,a,b,c]
join _ _ (prod s1 s2 a b) (prod s1 s3 a c)
--> prod s1 (sup s2 s3) a (x : T s1 a => join s2 s3 (b x) (c x)).
def cast : s1 : Sort -> s2 : Sort -> a : U s1 -> b : U s2 -> T s1 a -> T (sup s1 s2) (join s1 s2 a b).
[s1,s2,m]
cast _ _ (sort s1) (sort s2) m
--> lift s1 s2 m.
(;[s1 : Sort, s2 : Sort, s3 : Sort, s4 : Sort, a : U s1, b : U s3, m : T s1 a];)
(;cast {sup s1 s2} {sup s3 s4} (lift s1 s2 a) (lift s3 s4 b) m;)
(;--> cast s1 s3 a b m.;)
[s1,s2,s3,a,b,c,m]
cast _ _ (prod s1 s2 a b) (prod s1 s3 a c) m
--> x : T s1 a => cast s2 s3 (b x) (c x) (m x).
(; Aliases for readibility ;)
def Prop := U prop.
def Set := U set.
def Type0 := U (type z).
def Type1 := U (type (s z)).
......@@ -46,10 +46,10 @@ def rule' : Term -> Term -> Term.
def V := N.
var : V -> N.
var : V -> N -> N.
def normalize : Term -> Term.
def normalize2 : Term -> Term.
def normalize : N -> N.
def normalize2 : N -> N.
def minus : V -> V -> Ind.
[n] minus n 0 --> n
......@@ -63,9 +63,9 @@ def U3 : V -> N -> Term.
[k] U3 k 0 --> 0'
[k,x] U3 k (S x) --> S' (U3 k x).
def U2 : V -> Sort -> Term.
[k,f] U2 k (forall (x => f x)) --> Lam (U2 (S k) (f (var (S k))))
[k,x] U2 k (poly x) --> normalize2 (normalize (U3 k x)).
def U2 : V -> Sort -> N.
[k,f] U2 k (forall (x => f x)) --> x => (U2 (S k) (f (var (S k) x)))
[k,x] U2 k (poly x) --> normalize2 (normalize (U3 x).
def U : Sort -> Term := U2 0.
......@@ -128,48 +128,48 @@ def lexi_lt : Term -> Term -> Term -> Term -> Bool.
[x,y,z,t] lt (plus' z t) (rule' x y) --> F.
[] normalize 0' --> 0'
[x] normalize (S' x) --> S' (normalize x)
[] normalize 0 --> 0
[x] normalize (S x) --> S (normalize x)
[i] normalize (db i) --> db i
[x,y,z] normalize (max' (max' x y) z) --> normalize (max' x (max' y z))
[x,y,z] normalize (plus' (plus' x y) z) --> normalize (plus' x (plus' y z))
[x,y] normalize (plus' x y) -->
[x,y,z] normalize (max (max x y) z) --> normalize (max x (max y z))
[x,y,z] normalize (plus (plus x y) z) --> normalize (plus x (plus y z))
[x,y] normalize (plus x y) -->
(z : Term => t : Term =>
ite (lt z t)
(plus' z t)
(plus' t z)) (normalize x) (normalize y)
[x,y] normalize (max' x y) -->
(plus z t)
(plus t z)) (normalize x) (normalize y)
[x,y] normalize (max x y) -->
(z : Term => t : Term =>
ite (lt z t)
(max' z t)
(max' t z)) (normalize x) (normalize y).
(max z t)
(max t z)) (normalize x) (normalize y).
[x] plus' 0' x --> x.
[x,y] plus' (S' x) y --> S' (plus' x y).
[x,y] plus' x (S' y) --> S' (plus' x y).
[x] plus 0 x --> x.
[x,y] plus (S x) y --> S (plus x y).
[x,y] plus x (S y) --> S (plus x y).
[x] max' 0' x --> x.
[x,y] S' (max' x y) --> max' (S' x) (S' y).
[x] max 0 x --> x.
[x,y] S (max x y) --> max (S x) (S y).
[i,j,k] plus' i (max' j k) --> max' (plus' i j) (plus' i k).
[i,j,k] plus' (max' j k) i --> max' (plus' j i) (plus' k i).
[i,j,k] plus i (max j k) --> max (plus i j) (plus i k).
[i,j,k] plus (max j k) i --> max (plus j i) (plus k i).
def ltei : Term -> Term -> Bool.
[x] ltei x x --> T.
[a,b,c,d] ltei (plus' a b) (plus' c d) --> or (and (ltei a c) (ltei b d)) (ltei (plus' a b) d).
[x,y,z] ltei x (plus' y z) --> or (ltei x y) (ltei x z).
[x,y,z] ltei x (max' y z) --> or (ltei x y) (ltei x z).
[x,y] ltei (S' x) (S' y) --> ltei x y.
[x,y] ltei x (S' y) --> ltei x y.
[a,b,c,d] ltei (plus a b) (plus c d) --> or (and (ltei a c) (ltei b d)) (ltei (plus a b) d).
[x,y,z] ltei x (plus y z) --> or (ltei x y) (ltei x z).
[x,y,z] ltei x (max y z) --> or (ltei x y) (ltei x z).
[x,y] ltei (S x) (S y) --> ltei x y.
[x,y] ltei x (S y) --> ltei x y.
[x,y] ltei x y --> F.
[x,z] normalize2 (max' x z) --> ite (ltei x z) (normalize2 z) (max' x (normalize2 z)).
[x,z] normalize2 (max x z) --> ite (ltei x z) (normalize2 z) (max x (normalize2 z)).
[x] normalize2 (S' x) --> S' (normalize2 x).
[x] normalize2 (S x) --> S (normalize2 x).
[x,y] normalize2 (plus' x y) --> plus' (normalize2 x) (normalize2 y).
[x,y] normalize2 (plus x y) --> plus (normalize2 x) (normalize2 y).
[x] normalize2 (db x) --> db x.
......
#NAME cc.
Sort : Type.
0 : Sort.
1 : Sort.
defac plus [Sort].
[i] plus i 0 --> i.
defac max [Sort].
[i,j,k] max (plus i k) (plus i j) --> plus i (max j k)
[i,j ] max i (plus i j) --> plus i j
[i,j ] max (plus i j) i --> plus i j
[i ] max i i --> i
[i ] max 0 i --> i.
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[j ] rule 0 j --> j
[i ] rule i i --> i
[i,j] rule i (plus 1 j) --> max i (plus 1 j)
[i ] rule i 1 --> max i 1
[i,j] rule i (plus i j) --> plus i j
[i,j] rule (plus 1 i) j --> max (plus 1 i) j.
[i,j,k] max (rule i j) (rule i k) --> rule i (max j k).
[i,j,k] max (rule j i) (rule k i) --> rule (max j k) i.
#SNF u : Sort => v : Sort => w : Sort => max (plus u v) (plus u w).
#SNF x : Sort => y : Sort => rule 0 (rule (plus (plus x 1) (plus y 0)) (plus (plus 0 (plus 0 1)) (plus x y))).
#SNF x : Sort => y : Sort => rule (rule (plus (plus x 1) (plus y 0)) (plus (plus 0 (plus 0 1)) (plus x y))) 0.
#SNF i : Sort => rule (plus 1 i) 1.
U : Sort -> Type.
u : i : Sort -> U (plus i 1).
lift : i : Sort -> a : U i -> U (plus i 1).
def lnlift : n : Sort -> i : Sort -> a : U n -> U (plus n i).
[n,a] lnlift n 0 a --> a
[n,i,a] lnlift n (plus i 1) a --> lift (plus n i) (lnlift n i a).
def llift : i : Sort -> a : U 0 -> U i := lnlift 0.
def T : i : Sort -> a : U i -> Type.
[i,k] T k (u i) --> U i
[i,k,a] T k (lift i a) --> T i a
[i,k,a] T k (llift i a) --> T 0 a. (; This rule deduces from above. ;)
def prod :
i : Sort ->
j : Sort ->
a : U i ->
b : (x : T i a -> U j) ->
U (rule i j).
[i,a,b] T 0 (prod i 0 a b) --> x : T i a -> T 0 (b x)
(;
[i,j,a,b] T _ (prod i (plus i j) a b)
--> x: T i a -> T (plus i j) (b x)
[i,j,a,b] T _ (prod i i a b)
--> x: T i a -> T i (b x)
[i,j,a,b] T _ (prod 0 j a b)
--> x: T 0 a -> T j (b x)
[i,j,a,b] T _ (prod (plus (plus i j) 1) (plus j 1) a b)
--> x : T (plus (plus i j) 1) a -> T (plus j 1) (b x).
[i,j,a,b] T _ (prod (plus (plus i j) 1) (plus j 1) a b)
--> x : T (plus (plus i j) 1) a -> T (plus j 1) (b x).
;)
[i,j,a,b] T _ (prod i j a b) --> x : T i a -> T j (b x).
[i,j,a,b] prod _ (plus (plus i j) 1) (lift i a) b
--> prod i (plus (plus i j) 1) a b
[i,j,a,b] prod _ (plus j 1) (lift (plus (plus i j) 1) a) b
--> lift (plus (plus i j) 1) (prod (plus (plus i j) 1) (plus j 1) a b)
[i,j,a,b] prod (plus (plus i j ) (plus 1 1)) _ a (x => lift (plus j 1) (b x))
--> prod (plus (plus i j) (plus 1 1)) (plus j 1) a (x => b x)
[i,j,a,b] prod i _ a (x => lift (plus i j) (b x))
--> lift (plus i j) (prod i (plus i j) a (x => b x))
[i,a,b] prod (plus i 1) 1 a (x => lift 0 (b x))
--> llift (plus i 1) (prod (plus i 1) 0 a (x => b x))
[a,b] prod 0 1 a (x => lift 0 (b x))
--> lift 0 (prod 0 0 a (x => b x))
(; Why not merge the two above ? ;)
[i,a,b] prod (plus i 1) 0 (lift i a) b
--> prod i 0 a b.
#NAME cic.
Nat : Type.
z : Nat.
s : Nat -> Nat.
def m : Nat -> Nat -> Nat.
[i : Nat] m i z --> i.
[j : Nat] m z j --> j.
[i : Nat, j : Nat] m (s i) (s j) --> s (m i j).
(; Sorts ;)
Sort : Type.
prop : Sort.
type : Nat -> Sort.
(; Universe successors ;)
def succ : Sort -> Sort.
[] succ prop --> type z.
[i : Nat] succ (type i) --> type (s i).
(; Universe cumulativity ;)
def next : Sort -> Sort.
[] next prop --> type z.
[i : Nat] next (type i) --> type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort.
[s1 : Sort] rule s1 prop --> prop.
[s2 : Sort] rule prop s2 --> s2.
[i : Nat, j : Nat] rule (type i) (type j) --> type (m i j).
def max : Sort -> Sort -> Sort.
[s1 : Sort] max s1 prop --> s1.
[s2 : Sort] max prop s2 --> s2.
[i : Nat, j : Nat] max (type i) (type j) --> type (m i j).
(; Types and terms ;)
Univ : s : Sort -> Type.
def Term : s : Sort -> a : Univ s -> Type.
univ : s : Sort -> Univ (succ s).
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (max s1 s2).
def prod : s1 : Sort -> s2 : Sort -> a : Univ s1 -> b : (Term s1 a -> Univ s2) -> Univ (rule s1 s2).
[s : Sort] Term _ (univ s) --> Univ s.
[s1 : Sort, s2 : Sort, a : Univ s1] Term _ (lift s1 s2 a) --> Term s1 a.
[s1 : Sort, s2 : Sort, a : Univ s1, b : (Term s1 a -> Univ s2)]
Term _ (prod s1 s2 a b) --> x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
[s : Sort] max s s --> s.
[s1 : Sort, s2 : Sort, s3 : Sort] max (max s1 s2) s3 --> max s1 (max s2 s3).
[s1 : Sort, s2 : Sort, s3 : Sort] rule (max s1 s3) s2 --> max (rule s1 s2) (rule s3 s2).
[s1 : Sort, s2 : Sort, s3 : Sort] rule s1 (max s2 s3) --> max (rule s1 s2) (rule s1 s3).
[s : Sort, a : Univ s] lift s s a --> a.
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1]
lift _ s3 (lift s1 s2 a) -->
lift s1 (max s2 s3) a.
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1, b : Term s1 a -> Univ s2]
prod _ s2 (lift s1 s3 a) b -->
lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
[s1 : Sort, s2 : Sort, s3 : Sort, a : Univ s1, b : Term s1 a -> Univ s2]
prod s1 _ a (x => lift s2 s3 (b x)) -->
lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
#NAME cc.
Sort : Type.
0 : Sort.
1 : Sort.
defac plus [Sort].
[i] plus i 0 --> i.
defac max [Sort].
[i,j,k] max (plus i k) (plus i j) --> plus i (max j k)
[i,j ] max i (plus i j) --> plus i j
[i,j ] max (plus i j) i --> plus i j
[i ] max i i --> i
[i ] max 0 i --> i.
def rule : Sort -> Sort -> Sort.
[i ] rule i 0 --> 0
[j ] rule 0 j --> j
[i ] rule i i --> i
[i,j] rule i (plus 1 j) --> max i (plus 1 j)
[i ] rule i 1 --> max i 1
[i,j] rule i (plus i j) --> plus i j
[i,j] rule (plus 1 i) j --> max (plus 1 i) j.
[i,j,k] max (rule i j) (rule i k) --> rule i (max j k).
[i,j,k] max (rule j i) (rule k i) --> rule (max j k) i.
#SNF u : Sort => v : Sort => w : Sort => max (plus u v) (plus u w).
#SNF x : Sort => y : Sort => rule 0 (rule (plus (plus x 1) (plus y 0)) (plus (plus 0 (plus 0 1)) (plus x y))).
#SNF x : Sort => y : Sort => rule (rule (plus (plus x 1) (plus y 0)) (plus (plus 0 (plus 0 1)) (plus x y))) 0.
#SNF i : Sort => rule (plus 1 i) 1.
U : Sort -> Type.
u : i : Sort -> U (plus i 1).
lift : i : Sort -> a : U i -> U (plus i 1).
def lnlift : n : Sort -> i : Sort -> a : U n -> U (plus n i).
[n,a] lnlift n 0 a --> a
[n,i,a] lnlift n (plus i 1) a --> lift (plus n i) (lnlift n i a).
def llift : i : Sort -> a : U 0 -> U i := lnlift 0.
def T : i : Sort -> a : U i -> Type.
[i,k] T k (u i) --> U i
[i,k,a] T k (lift i a) --> T i a
[i,k,a] T k (llift i a) --> T 0 a. (; This rule deduces from above. ;)
def prod :
i : Sort ->
j : Sort ->
a : U i ->
b : (x : T i a -> U j) ->
U (rule i j).
[i,a,b] T 0 (prod i 0 a b) --> x : T i a -> T 0 (b x)
(;
[i,j,a,b] T _ (prod i (plus i j) a b)
--> x: T i a -> T (plus i j) (b x)
[i,j,a,b] T _ (prod i i a b)
--> x: T i a -> T i (b x)
[i,j,a,b] T _ (prod 0 j a b)
--> x: T 0 a -> T j (b x)
[i,j,a,b] T _ (prod (plus (plus i j) 1) (plus j 1) a b)
--> x : T (plus (plus i j) 1) a -> T (plus j 1) (b x).
[i,j,a,b] T _ (prod (plus (plus i j) 1) (plus j 1) a b)
--> x : T (plus (plus i j) 1) a -> T (plus j 1) (b x).
;)
[i,j,a,b] T _ (prod i j a b) --> x : T i a -> T j (b x).
[i,j,a,b] prod _ (plus (plus i j) 1) (lift i a) b
--> prod i (plus (plus i j) 1) a b
[i,j,a,b] prod _ (plus j 1) (lift (plus (plus i j) 1) a) b
--> lift (plus (plus i j) 1) (prod (plus (plus i j) 1) (plus j 1) a b)
[i,j,a,b] prod (plus (plus i j ) (plus 1 1)) _ a (x => lift (plus j 1) (b x))
--> prod (plus (plus i j) (plus 1 1)) (plus j 1) a (x => b x)
[i,j,a,b] prod i _ a (x => lift (plus i j) (b x))
--> lift (plus i j) (prod i (plus i j) a (x => b x))
[i,a,b] prod (plus i 1) 1 a (x => lift 0 (b x))
--> llift (plus i 1) (prod (plus i 1) 0 a (x => b x))
[a,b] prod 0 1 a (x => lift 0 (b x))
--> lift 0 (prod 0 0 a (x => b x))
(; Why not merge the two above ? ;)
[i,a,b] prod (plus i 1) 0 (lift i a) b
--> prod i 0 a b.
#NAME idic.
def Top_3 := cc.1.
def Top_48 := cc.2.
def Top_49 := cc.1.
def id : A : cc.U Top_3 -> cc.T Top_3 A -> cc.T Top_3 A :=
A => x => x.
def pid : s : cc.Sort -> t : cc.U s -> cc.T s t -> cc.T s t
:= s => t => x => x.
def aux : A : cc.U Top_49 -> cc.T Top_49 A -> cc.T Top_49 A :=
pid Top_48
(cc.prod
Top_48
Top_49
(cc.u Top_49)
(A => cc.prod Top_49 Top_49 A (x => A)))
id.
def paux : Top_52 : cc.Sort ->
Top_53 : cc.Sort ->
prf (lt Top_3 Top_52) ->
prf (eq Top_3 Top_53) ->
A : cc.U Top_53 -> cc.T Top_53 A -> cc.T Top_53 A :=
Top_52 : cc.Sort =>
Top_53 : cc.Sort =>
pid Top_52
(cc.prod
Top_52 (; (cc.plus cc.1 Top_53) Top_52 ;)
Top_53
(magic (cc.plus cc.1 Top_53) Top_52 (cc.u Top_53))
(A (; T Top_52 (lift (u Top_53)) ;) =>
cc.prod Top_53 Top_53 A (x => A))) (; A -> A : Type@{Top_53} ;)
id.
(;
def 2 := cc.plus cc.1 cc.1.
def 3 := cc.plus cc.1 2.
def 4 := cc.plus cc.1 3.
def 5 := cc.plus cc.1 4.
#SNF a : cc.Sort => b : cc.Sort => c : cc.Sort =>
(cc.max
(cc.max
(cc.plus a 2)
(cc.plus (cc.plus a 3) b))
(cc.plus a (cc.max 5 (cc.plus 4 c)))).
;)
\ No newline at end of file
Set Printing Universes.
Definition id {A : Type} (a : A) := a.
About id.
Polymorphic Definition pid {A : Type} (a : A) := a.
About pid.
Definition aux := @pid (forall A:Type,A->A) (@id).
Print aux.
Polymorphic Definition paux := @pid (forall A:Type,A->A) (@id).
Print paux.
Polymorphic Definition paux2 := pid (@id).
Print paux2.
Print Universes.
Print Sorted Universes.
#NAME cic.
def Nat : Type := cc.Sort.
def z : Nat := cc.0.
def s : Nat -> Nat := x => cc.plus cc.1 x.
def m : Nat -> Nat -> Nat := cc.max.
#CONV i : Nat => m i z , i : Nat => i.
#CONV j : Nat => m z j , j : Nat => j.
#CONV i : Nat => j : Nat => m (s i) (s j) , i : Nat => j : Nat => s (m i j).
(; Sorts ;)
def Sort : Type := cc.Sort.
def prop : Sort := cc.0.
def type : Nat -> Sort := s.
(; Universe successors ;)
def succ : Sort -> Sort := s.
#CONV succ prop, type z.
#CONV i : Nat => succ (type i), i : Nat => type (s i).
(; Universe cumulativity ;)
def next : Sort -> Sort := s.
#CONV next prop, type z.
#CONV i : Nat => next (type i), i : Nat => type (s i).
(; Universe product rules ;)
def rule : Sort -> Sort -> Sort := cc.rule.
#CONV s1 : Sort => rule s1 prop, s1 : Sort => prop.
#CONV s2 : Sort => rule prop s2, s2 : Sort => s2.
#CONV i : Nat => j : Nat => rule (type i) (type j), i : Nat => j : Nat => type (m i j).
def max : Sort -> Sort -> Sort := cc.max.
#CONV s1 : Sort => max s1 prop, s1 : Sort => s1.
#CONV s2 : Sort => max prop s2, s2 : Sort => s2.
#CONV i : Nat => j : Nat => max (type i) (type j), i : Nat => j : Nat => type (m i j).
(; Types and terms ;)
def Univ : s : Sort -> Type := cc.U.
def Term : s : Sort -> a : Univ s -> Type := cc.T.
def univ : s : Sort -> Univ (succ s) := cc.u.
def lift : s1 : Sort -> s2 : Sort -> a : Univ s1 -> Univ (max s1 s2).
[i ,a] lift i i a --> a
[i,j,a] lift i (cc.plus i j) a --> cc.lnlift i j a
[i,j,a] lift (cc.plus i j) i a --> a.
def prod : s1 : Sort ->
s2 : Sort ->
a : Univ s1 ->
b : (Term s1 a -> Univ s2) ->
Univ (rule s1 s2) := cc.prod.
#CONV s : Sort => Term (succ s) (univ s), s : Sort => Univ s.
#CONV s1 : Sort => s2 : Sort => a : Univ s1 => Term (max s1 s2) (lift s1 s2 a),
s1 : Sort => s2 : Sort => a : Univ s1 => Term s1 a.
#CONV s1 : Sort => s2 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) =>
Term (rule s1 s2) (prod s1 s2 a b),
s1 : Sort => s2 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) =>
x : Term s1 a -> Term s2 (b x).
(; Canonicity rules ;)
#CONV s : Sort => max s s, s : Sort => s.
#CONV s1 : Sort => s2 : Sort => s3 : Sort => max (max s1 s2) s3,
s1 : Sort => s2 : Sort => s3 : Sort => max s1 (max s2 s3).
#CONV s1 : Sort => s2 : Sort => s3 : Sort => rule (max s1 s3) s2,
s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s3 s2).
#CONV s1 : Sort => s2 : Sort => s3 : Sort => rule s1 (max s2 s3),
s1 : Sort => s2 : Sort => s3 : Sort => max (rule s1 s2) (rule s1 s3).
#CONV s : Sort => a : Univ s => lift s s a,
s : Sort => a : Univ s => a.
#CONV s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => lift (max s1 s2) s3 (lift s1 s2 a),
s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => lift s1 (max s2 s3) a.
#CONV s1 : Sort=> s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => prod (max s1 s3) s2 (lift s1 s3 a) b,
s1 : Sort=> s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => lift (rule s1 s2) (rule s3 s2) (prod s1 s2 a b).
#CONV s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => prod s1 _ a (x => lift s2 s3 (b x)),
s1 : Sort => s2 : Sort => s3 : Sort => a : Univ s1 => b : (Term s1 a -> Univ s2) => lift (rule s1 s2) (rule s1 s3) (prod s1 s2 a (x => b x)).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment