Commit fbd1a896 authored by Gaspard Ferey's avatar Gaspard Ferey

Work on Coq model.

parent 852beb20
......@@ -13,7 +13,7 @@ def max : N -> N -> N.
B : Type.
true : B.
true : B.
false : B.
defac and [B].
......@@ -108,3 +108,8 @@ constrain : d : Cstr -> c : Cstr -> i : N -> a : U c i -> U (and d c) i.
a
(x => constrain (le j k) d j (b x))
).
def u' : c : Cstr -> i : N -> U c (s i) := c => i => constrain c true (s i) (u i).
def u'' : c : Cstr -> i : N -> j : N -> U (and c (le (s i) j)) j :=
c => i => j => lift c (s i) j (u' c i).
\ No newline at end of file
#NAME idic.
def 0 := cc.0.
def 1 := cc.s 0.
def 2 := cc.s 1.
def Cstr := cc.Cstr.
def s := cc.s.
def Sort := cc.N.
def Set := 0.
def Set := cc.0.
def sle := i:Sort => j:Sort => cc.le (cc.s i) j.
def and := cc.and.
......@@ -48,14 +46,9 @@ Prop < Set
;)
def Top_1 : Sort.
def global : cc.Cstr :=
(and (sle Set Top_1)
cc.true
)
.
def g1 : Cstr.
def global : Cstr := g1.
(;
......@@ -63,10 +56,15 @@ id = fun (A : Type@{Top.1}) (a : A) => a
: forall A : Type@{Top.1}, A -> A
(* Top.1 |= *)
;)
def Top_1 : Sort.
def g2 : Cstr.
[] g1 --> (and (sle Set Top_1) g2).
def id :
A : cc.U global Top_1 ->
cc.T global Top_1 A ->
cc.T global Top_1 A := A => x => x.
cc.T global Top_1 A := c => A => x => x.
(;
......@@ -75,26 +73,43 @@ fun (A : Type@{Top.2}) (a : A) => a
: forall A : Type@{Top.2}, A -> A
(* Top.2 |= *)
;)
def pid : Top_2 : cc.Sort ->
A : cc.U Top_2 -> cc.T Top_2 A -> cc.T Top_2 A :=
Top_2 => A => x => x.
def pid :
c : Cstr ->
Top_2 : Sort ->
A : cc.U (and c global) Top_2 ->
cc.T c Top_2 A ->
cc.T c Top_2 A := c => Top_2 => A => x => x.
(;
pid_id = pid@{Top.3} (@id)
: forall A : Type@{Top.1}, A -> A
(* Top.3 |= Top.1 < Top.3
*)
pid_id = pid@{Top.3} (@id) : forall A : Type@{Top.1}, A -> A
(* Top.3 |= Top.1 < Top.3 *)
;)
def Top_3 := 2.
def pid_id : A : cc.U Top_1 -> cc.T Top_1 A -> cc.T Top_1 A :=
pid Top_3
def Top_3 : Sort.
def pid_id :
c : Cstr ->
A : cc.U c Top_1 ->
cc.T c Top_1 A ->
cc.T (and (sle Top_1 Top_3) c) Top_1 A
:=
c : Cstr =>
pid (and (sle Top_1 Top_3) c) Top_3
(cc.prod
Top_3
Top_1
(cc.u Top_1)
(A => cc.prod Top_1 Top_1 A (x => A)))
(and (sle Top_1 Top_3) c)
Top_3
(and (sle Top_1 Top_3) c)
Top_3
(cc.u'' c Top_1 Top_3)
(A => cc.prod
c
Top_1
c
Top_1
A
(x => A)))
id.
(;
......
Set Printing Universes.
Definition id {A : Type} (a : A) := a.
Polymorphic Definition pid {A : Type} (a : A) := a.
......@@ -14,6 +16,4 @@ Polymorphic Definition p_pid_id_expl := @pid (forall A:Type,A->A) (@id).
Polymorphic Definition p_pid_pid := pid (@pid).
Polymorphic Definition p_pid_pid_expl := @pid (forall A:Type,A->A) (@pid).
Set Printing Universes.
Print Universes.
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