Commit 52fc15a3 authored by Francois THIRE's avatar Francois THIRE

Add a better version of itt.

parent 4ce7f8c5
#NAME itt.
(; Universes ;)
level : Type.
Z : level.
S : level -> level.
U : level -> Type.
def max : level -> level -> level.
[x] max Z x --> x
[x] max x Z --> x
[x,y] max (S x) (S y) --> S (max x y).
def Term : i:level -> U i -> Type.
(; Types ;)
univ : i:level -> U (S i).
lift : i : level -> j : level -> U i -> U (max i j).
prod : i : level -> A : U i -> (Term i A -> U i) -> U i.
sigma : i : level -> A : U i -> (Term i A -> U i) -> U i.
sum : i : level -> U i -> U i -> U i.
void : U Z.
unit : U Z.
nat : U Z.
eq : i : level -> A:U i -> Term i A -> Term i A -> U i.
(; ad-hoc rewrite rules on Term for universes and lambda ;)
[i] Term _ (univ i) --> U i
[i,j,t] Term _ (lift i j t) --> Term i t
[i,A,f] Term _ (prod i A f) --> x:Term i A -> Term i (f x).
(; Constructors ;)
pair : i : level -> A : U i -> B : (Term i A -> U i) -> a : Term i A -> Term i (B a) -> Term i (sigma i A B).
inl : i : level -> A : U i -> B : U i -> Term i A -> Term i (sum i A B).
inr : i : level -> A : U i -> B : U i -> Term i B -> Term i (sum i A B).
star : Term Z unit.
0 : Term Z nat.
s : Term Z nat -> Term Z nat.
refl : i : level -> A : U i -> x:Term i A -> Term i (eq i A x x).
(; Induction principles ;)
def ind_sigma : i : level -> A : U i -> B : (Term i A -> U i) ->
C : (Term i (sigma i A B) -> U i) ->
g: (x :Term i A -> y : Term i (B x) -> Term i (C (pair i A B x y))) ->
p : (Term i (sigma i A B)) -> Term i (C p).
def ind_sum : i : level -> A : U i -> B : U i -> C : (Term i (sum i A B) -> U i) ->
c : (x : Term i A -> Term i (C (inl i A B x))) ->
d : (y : Term i B -> Term i (C (inr i A B y))) ->
p : (Term i (sum i A B)) -> Term i (C p).
ind_void : i : level -> C : (Term Z void -> U i) -> a : Term Z void -> Term i (C a).
def ind_unit : i : level -> C : (Term Z unit -> U i) -> c : (Term i (C star)) -> a : Term Z unit -> Term i (C a).
def ind_nat : i : level -> C : (Term Z nat -> U i) -> c0 : (Term i (C 0)) -> cs : (x:Term Z nat -> y : Term i (C x) -> Term i (C (s x))) -> n : Term Z nat -> Term i (C n).
def ind_eq : i : level -> A : U i -> C : (x:Term i A -> y:Term i A -> Term i (eq i A x y) -> U i) -> c : (z:Term i A -> Term i (C z z (refl i A z))) ->
x:Term i A -> y:Term i A -> p:Term i (eq i A x y) -> Term i (C x y p).
(; Computational rules ;)
[i,A,B,C,g,a,b] ind_sigma i A B C g (pair i A B a b) --> g a b.
[i,A,B,C,c,d,x] ind_sum i A B C c d (inl i A B x) --> c x.
[i,A,B,C,c,d,y] ind_sum i A B C c d (inr i A B y) --> d y.
[i,C,c] ind_unit i C c star --> c.
[i,C,c0,cs] ind_nat i C c0 cs 0 --> c0.
[i,C,c0,cs,n] ind_nat i C c0 cs (s n) --> cs n (ind_nat i C c0 cs n).
[i,A,C,c,a] ind_eq i A C c a a (refl i A a) --> c a.
\ No newline at end of file
#NAME itt.
level : Type.
Z : level.
S : level -> level.
U : level -> Type.
def max : level -> level -> level.
[x] max Z x --> x
[x] max x Z --> x
[x,y] max (S x) (S y) --> S (max x y).
def Term : i:level -> U i -> Type.
univ : i:level -> U (S i).
lift : i : level -> j : level -> U i -> U (max i j).
prod : i : level -> A : U i -> (Term i A -> U i) -> U i.
sigma : i : level -> A : U i -> (Term i A -> U i) -> U i.
coprod : i : level -> U i -> U i -> U i.
void : U Z.
unit : U Z.
nat : U Z.
eq : i : level -> A:U i -> Term i A -> Term i A -> U i.
[i] Term _ (univ i) --> U i
[i,j,t] Term _ (lift i j t) --> Term i t
[i,A,f] Term _ (prod i A f) --> x:Term i A -> Term i (f x)
[i,A,f] Term _ (sigma i A f) --> j : level -> C : U j -> (x:Term i A -> Term i (f x) -> Term j C) -> Term j C
[i,A,B] Term _ (coprod i A B) --> j : level -> C:U j -> (Term i A -> Term j C) -> (Term i B -> Term j C) -> Term j C
[] Term _ (void) --> i : level -> A:U i -> Term i A
[] Term _ (unit) --> i : level -> A:U i -> Term i A -> Term i A
[] Term _ (nat) --> i : level -> A:U i -> Term i A -> (Term i A -> Term i A) -> Term i A
[i,A,a,b] Term _ (eq i A a b) --> j : level -> P : (Term i A -> U j) -> Term j (P a) -> Term j (P b).
def I : Term Z unit := i => A => x => x.
def z : Term Z nat := i => A => z => s => z.
def s : Term Z nat -> Term Z nat := x => i => A => z => s => s (x i A z s).
def refl : i : level -> A:U i -> a:Term i A -> Term i (eq i A a a) := i => A => a => j => P => x => x.
\ No newline at end of file
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