Commit 4ce7f8c5 authored by Francois THIRE's avatar Francois THIRE

Add an encoding of itt that might not work

parent 2bfe295f
#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