pair-eta/syntax.sig

nat  : Type
Tm(VarTm) : Type
PTag : Type
TTag : Type
bool : Type

TPi : TTag
TSig : TTag
PL : PTag
PR : PTag
Abs : (bind Tm in Tm) -> Tm
App : Tm -> Tm -> Tm
Pair : Tm -> Tm -> Tm
Proj : PTag -> Tm -> Tm
TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm
Bot : Tm
Univ : nat -> Tm
Bool : Tm
BVal : bool -> Tm
If : Tm -> Tm -> Tm -> Tm
Prove join univ pi contra 2024-12-25 21:11:58 -05:00			`nat : Type`
Initial commit 2024-12-11 23:52:57 -05:00			`Tm(VarTm) : Type`
Simplify the syntax by combining proj1 and proj2 2024-12-22 10:38:58 -05:00			`PTag : Type`
Generalize Pi to TBind so we have both sigma and pi 2024-12-27 12:12:19 -05:00			`TTag : Type`
Initial commit (still tweaking the rules) 2025-01-10 16:51:49 -05:00			`bool : Type`
Initial commit 2024-12-11 23:52:57 -05:00
Generalize Pi to TBind so we have both sigma and pi 2024-12-27 12:12:19 -05:00			`TPi : TTag`
			`TSig : TTag`
Simplify the syntax by combining proj1 and proj2 2024-12-22 10:38:58 -05:00			`PL : PTag`
			`PR : PTag`
Initial commit 2024-12-11 23:52:57 -05:00			`Abs : (bind Tm in Tm) -> Tm`
			`App : Tm -> Tm -> Tm`
			`Pair : Tm -> Tm -> Tm`
Simplify the syntax by combining proj1 and proj2 2024-12-22 10:38:58 -05:00			`Proj : PTag -> Tm -> Tm`
Generalize Pi to TBind so we have both sigma and pi 2024-12-27 12:12:19 -05:00			`TBind : TTag -> Tm -> (bind Tm in Tm) -> Tm`
Prove join univ pi contra 2024-12-25 21:11:58 -05:00			`Bot : Tm`
Combine the different prov cases into one function 2024-12-29 22:33:37 -05:00			`Univ : nat -> Tm`
Initial commit (still tweaking the rules) 2025-01-10 16:51:49 -05:00			`Bool : Tm`
			`BVal : bool -> Tm`
			`If : Tm -> Tm -> Tm -> Tm`