From 8607a41482d90f917d435a9eff3fa49f751b9ac9 Mon Sep 17 00:00:00 2001 From: Anders Date: Mon, 8 Jun 2015 14:42:23 +0200 Subject: [PATCH] Make bool, circle and integer compile --- examples/bool.ctt | 16 ++++++++-------- examples/circle.ctt | 2 +- examples/integer.ctt | 7 ++++++- examples/interval.ctt | 37 ------------------------------------- examples/newhedberg.ctt | 33 +++++++++++++++------------------ 5 files changed, 30 insertions(+), 65 deletions(-) diff --git a/examples/bool.ctt b/examples/bool.ctt index 9dcc6ba..299ba60 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -13,9 +13,9 @@ negBoolK : (b : bool) -> Id bool (negBool (negBool b)) b = split true -> refl bool true negBoolEq : Id U bool bool = - glue bool [ (i = 0) -> (bool,negBool,negBool,negBoolK,negBoolK) ] + isoId bool bool negBool negBool negBoolK negBoolK -test : bool = transport negBoolEq true +test : bool = trans bool bool negBoolEq true data F2 = zeroF2 | oneF2 @@ -53,12 +53,12 @@ negBool' : bool -> bool = subst U (\(X : U) -> (X -> X)) F2 bool F2EqBool negF2 F2EqBoolComp : Id U F2 bool = compId U F2 bool bool F2EqBool negBoolEq -test2 : bool = transport F2EqBoolComp oneF2 +test2 : bool = trans F2 bool F2EqBoolComp oneF2 negNegEq : Id U bool bool = compId U bool bool bool negBoolEq negBoolEq -test3 : bool = transport negNegEq true +test3 : bool = trans bool bool negNegEq true test4 : Id U bool bool = negNegEq @ i kanBool : Id U bool bool = @@ -69,10 +69,10 @@ squareBoolF2 : Square U bool bool (refl U bool) bool F2 boolEqF2 @ i /\ j test5 : IdP boolEqF2 true oneF2 = - transport ( boolEqF2 @ i /\ j) true + comp ( boolEqF2 @ i /\ j) true [] test6 : Id bool true true = - transport ( F2EqBool @ i \/ j) (test5 @ - i) + comp ( F2EqBool @ i \/ j) (test5 @ - i) [] test7 : Id U F2 F2 = subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 negNegEq @@ -81,7 +81,7 @@ test8 : Id U F2 F2 = subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 (refl U bool) test9 : Id U F2 F2 = - transport ( Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) + comp ( Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool) [] -p : Id U F2 bool = comp (<_>U) bool [ (i = 0) -> boolEqF2 ] +p : Id U F2 bool = comp (<_> U) bool [ (i = 0) -> boolEqF2, (i = 1) -> <_> bool] q : Id U F2 F2 = p @ (i /\ - i) \ No newline at end of file diff --git a/examples/circle.ctt b/examples/circle.ctt index f12b45d..ea38957 100644 --- a/examples/circle.ctt +++ b/examples/circle.ctt @@ -20,7 +20,7 @@ helix : S1 -> U = split base -> Z loop @ i -> sucIdZ @ i -winding (p : loopS1) : Z = transport rem zeroZ +winding (p : loopS1) : Z = trans Z Z rem zeroZ where rem : Id U Z Z = helix (p @ i) diff --git a/examples/integer.ctt b/examples/integer.ctt index e100089..fdf55a5 100644 --- a/examples/integer.ctt +++ b/examples/integer.ctt @@ -60,7 +60,12 @@ p1 : T = compId int (pos zero) (neg zero) (pos zero) zeroP' (zeroP'@-i) test0 : Id (Id Z (inr zero) (inr zero)) (refl Z (inr zero)) (refl Z (inr zero)) = ZSet (inr zero) (inr zero) (refl Z (inr zero)) (refl Z (inr zero)) + +-- Tests for normal forms: test1 : Id T p0 p1 = intSet (pos zero) (pos zero) p0 p1 test2 : Id T p0 p0 = intSet (pos zero) (pos zero) p0 p0 -ntest2 : Id T p0 p0 = comp int (comp int (comp int (pos zero) [ (i1 = 0) -> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 0)(i4 = 1) -> comp int (pos zero) [ (i5 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> pos zero ] ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (comp int (pos zero) [ ]) [ (i7 = 0) -> comp int (pos zero) [ ] ] ], (i5 = 1) -> pos zero ], (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 0)(i4 = 1) -> comp int (pos zero) [ (i5 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> pos zero ] ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (comp int (pos zero) [ ]) [ (i7 = 0) -> comp int (pos zero) [ ] ] ], (i5 = 1) -> pos zero ], (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ], (i3 = 1) -> pos zero ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i4 = 0) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i7 = 1)(i8 = 1) -> pos zero, (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ] ], (i7 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ], (i9 = 0) -> pos zero ]) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> pos zero ], (i7 = 1) -> pos zero, (i8 = 0) -> pos zero ], (i7 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ]) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ] ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ] ] ], (i7 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i7 = 1)(i8 = 1) -> pos zero, (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ] ], (i7 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ], (i9 = 0) -> pos zero ]) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> pos zero ], (i7 = 1) -> pos zero, (i8 = 0) -> pos zero ], (i7 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ]) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ] ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ] ] ], (i7 = 1) -> pos zero ] ], (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1)(i7 = 1) -> comp int (pos zero) [ (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i8 = 1) -> pos zero ], (i7 = 0) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1)(i7 = 1) -> comp int (pos zero) [ (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i8 = 1) -> pos zero ], (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i6 = 0) -> comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ] ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i1 = 1) -> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 0)(i4 = 1) -> comp int (pos zero) [ (i5 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> pos zero ] ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (comp int (pos zero) [ ]) [ (i7 = 0) -> comp int (pos zero) [ ] ] ], (i5 = 1) -> pos zero ], (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ]) [ (i3 = 0)(i4 = 1) -> comp int (pos zero) [ (i5 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> pos zero ] ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (comp int (pos zero) [ ]) [ (i7 = 0) -> comp int (pos zero) [ ] ] ], (i5 = 1) -> pos zero ], (i3 = 1) -> pos zero, (i4 = 0) -> pos zero ], (i3 = 1) -> pos zero ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 1) -> pos zero ]) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i3 = 0) -> comp int (pos zero) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i4 = 0) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i7 = 1)(i8 = 1) -> pos zero, (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ] ], (i7 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ], (i9 = 0) -> pos zero ]) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> pos zero ], (i7 = 1) -> pos zero, (i8 = 0) -> pos zero ], (i7 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int(pos zero) [ (i9 = 0) -> pos zero ] ]) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ] ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ] ] ], (i7 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i7 = 1)(i8 = 1) -> pos zero, (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ] ], (i7 = 0) -> comp int (comp int (pos zero) [ (i6 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero ] ], (i6 = 0) -> pos zero, (i6 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i7 = 0) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ], (i9 = 0) -> pos zero ]) [ (i8 = 0) -> pos zero, (i8 = 1)(i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> pos zero ], (i7 = 1) -> pos zero, (i8 = 0) -> pos zero ], (i7 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero, (i9 = 0) -> pos zero ], (i9 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ]) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i8 = 0) -> pos zero, (i8 = 1) -> comp int (pos zero) [ (i9 = 0) -> pos zero ] ] ], (i8 = 0) -> pos zero, (i8 = 1) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ], (i9 = 0) -> comp int (pos zero) [ ] ], (i9 = 0) -> comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ] ] ], (i7 = 1) -> pos zero ] ], (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1)(i7 = 1) -> comp int (pos zero) [ (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i8 = 1) -> pos zero ], (i7 = 0) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i7 = 0) -> pos zero ]) [ (i6 = 0) -> pos zero, (i6 = 1)(i7 = 1) -> comp int (pos zero) [ (i8 = 0) -> comp int (comp int (pos zero) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (pos zero) [ (i10 = 0) -> pos zero ] ]) [ (i9 = 0) -> pos zero, (i9 = 1) -> comp int (comp int (pos zero) [ ]) [ (i10 = 0) -> comp int (pos zero) [ ] ] ], (i8 = 1) -> pos zero ], (i7 = 0) -> pos zero ], (i6 = 0) -> pos zero ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ] ]) [ (i2 = 0) -> pos zero, (i2 = 1) -> pos zero, (i6 = 0) -> comp int (pos zero) [ (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero ]) [ (i3 = 0) -> pos zero, (i3 = 1) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ] ] ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 0) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ], (i2 = 1) -> comp int (comp int (comp int (pos zero) [ (i3 = 1) -> pos zero ]) [ (i3 = 1) -> pos zero ]) [ (i3 = 0) -> comp int (pos zero) [ (i4 = 0) -> comp int (comp int (pos zero) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (pos zero) [ (i6 = 0) -> pos zero ] ]) [ (i5 = 0) -> pos zero, (i5 = 1) -> comp int (comp int (pos zero) [ ]) [ (i6 = 0) -> comp int (pos zero) [ ] ] ], (i4 = 1) -> pos zero ], (i3 = 1) -> pos zero ] ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> pos zero, (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ]) [ (i1 = 0) -> pos zero, (i1 = 1) -> pos zero, (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ] +ntest1 : Id T p0 p1 = comp (<_> int) (pos zero) [ (i1 = 0) -> pos zero, (i1 = 1) -> comp (<_> int) (zeroP {int} @ (i2 /\ i3)) [ (i2 = 0) -> pos zero, (i2 = 1) -> zeroP {int} @ (-i4 /\ i3), (i3 = 0) -> pos zero, (i3 = 1) -> comp (<_> int) (zeroP {int} @ i2) [ (i2 = 0) -> pos zero, (i2 = 1) -> zeroP {int} @ (-i4 \/ -i5), (i4 = 0) -> zeroP {int} @ i2 ] ], (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ] + +ntest2 : Id T p0 p0 = comp (<_> int) (pos zero) [ (i1 = 0) -> pos zero, (i1 = 1) -> pos zero, (i2 = 0) -> pos zero, (i2 = 1) -> pos zero ] + diff --git a/examples/interval.ctt b/examples/interval.ctt index 36dc6ae..50adb42 100644 --- a/examples/interval.ctt +++ b/examples/interval.ctt @@ -35,49 +35,12 @@ propI : prop I = subst U prop Unit I unitEqI propUnit setI : set I = subst U set Unit I unitEqI setUnit -foo (X : U) : U = (x : X) -> Id X x x - T : U = Id I zero zero p0 : T = refl I zero test : T = propI zero zero -fooI : foo I = subst U foo Unit I unitEqI (\(x : Unit) -> x) -test2 : T = fooI zero - --- ntest2 : T = comp I (comp I (comp I zero [ (i1 = 0) -> comp I (comp I (comp I zero [ ]) [ ]) [ (i2 = 0) -> comp I zero [ (i2 = 0) -> comp I zero [ (i2 = 0) -> zero, (i2 = 1) -> comp I (comp I zero [ ]) [ (i2 = 0) -> comp I zero [ ] ] ], (i2 = 1) -> zero ], (i2 = 1) -> zero ], (i1 = 1) -> comp I (comp I (comp I zero [ ]) [ ]) [ (i2 = 0) -> comp I zero [ (i2 = 0) -> comp I zero [ (i2 = 0) -> zero, (i2 = 1) -> comp I (comp I zero [ ]) [ (i2 = 0) -> comp I zero [ ] ] ], (i2 = 1) -> zero ], (i2 = 1) -> zero ] ]) [ (i1 = 0) -> zero, (i1 = 1) -> zero ]) [ (i1 = 0) -> zero, (i1 = 1) -> zero ] - --- test1 : T = comp I (comp I (comp I zero [ (i1 = 0) -> comp I (comp I (comp I zero [ ]) [ ]) [ (i2 = 0) -> comp I zero [ (i2 = 0) -> comp I zero [ (i2 = 0) -> zero, (i2 = 1) -> comp I (comp I zero [ ]) [ (i2 = 0) -> comp I zero [ ] ] ], (i2 = 1) -> zero ], (i2 = 1) -> zero ], (i1 = 1) -> comp I (comp I (comp I zero [ ]) [ ]) [ (i2 = 0) -> comp I zero [ (i2 = 0) -> comp I zero [ (i2 = 0) -> zero, (i2 = 1) -> comp I (comp I zero [ ]) [ (i2 = 0) -> comp I zero [ ] ] ], (i2 = 1) -> zero ], (i2 = 1) -> zero ] ]) [ (i1 = 0) -> zero, (i1 = 1) -> zero ]) [ (i1 = 0) -> zero, (i1 = 1) -> zero ] - - --- [ (i2 = 0) -> zero --- , (i2 = 1) -> comp (<_> I) (comp (<_> I) zero []) --- [ (i2 = 0) -> comp (<_> I) zero []]] - --- with zero - -test : Unit = transport ( unitEqI @ -i) zero -test' : IdP ( unitEqI @ -i) zero tt = - genComp ( unitEqI @ -i \/ -k) zero [(i = 0) -> <_> zero] -test'' : Id I zero zero = comp I - (comp I - (comp I zero [ (i0 = 0) -> zero ]) - [ (i0 = 0) -> zero ]) - [ (i0 = 0) -> zero, (i0 = 1) -> comp I zero [ (i1 = 0) -> comp I zero [ (i1 = 0) -> zero, (i1 = 1) -> comp I (comp I zero [ ]) [ (i1 = 0) -> comp I zero [ ] ] ], (i1 = 1) -> zero ] ] --- -- glueElem --- (comp I --- (comp I --- (comp I zero [ (i0 = 0) -> zero ]) --- [ (i0 = 0) -> zero ]) --- [ (i0 = 0) -> zero, (i0 = 1) -> comp I zero [ (i1 = 0) -> comp I zero [ (i1 = 0) -> zero, (i1 = 1) -> comp I (comp I zero [ ]) [ (i1 = 0) -> comp I zero [ ] ] ], (i1 = 1) -> zero ] ]) --- [ (i0 = 1) -> tt ] --- test : I = transport unitEqI tt --- eqttzero : IdP unitEqI tt zero = --- genComp ( unitEqI @ -i \/ -j) zero [(i=1) -> <_>zero] --- transport ( unitEqI @ -i \/ -j) zero --- genComp ( unitEqI @ i /\ j) tt [(i=0) -> tt] --- Type checking failed: path endpoints don't match for comp ( unitEqI @ (i /\ j)) tt [ ], got (tt,comp I (comp I (comp I zero [ ]) [ ]) [ ]), but expected (tt,zero) diff --git a/examples/newhedberg.ctt b/examples/newhedberg.ctt index 03bb539..158660e 100644 --- a/examples/newhedberg.ctt +++ b/examples/newhedberg.ctt @@ -4,15 +4,20 @@ import prelude hedbergLemma (A: U) (a b:A) (f : (x : A) -> Id A a x -> Id A a x) (p : Id A a b) : Square A a a (refl A a) a b p (f a (refl A a)) (f b p) = - transport (Square A a a (refl A a) a (p@i) (p@i/\j) (f a (refl A a)) (f (p@i) (p@i/\j))) - ((f a (refl A a))) + comp ( Square A a a (<_> a) a (p @ i) ( p @ i /\ j) + (f a (<_> a)) (f (p @ i) ( p @ i /\ j))) + ( f a (<_> a)) [] -hedberg (A:U) (a b:A) (h: (x:A) -> stable (Id A a x)) (p q : Id A a b) : Id (Id A a b) p q = - comp (<_> A) a [(j=0) -> rem2 @ i, (j=1) -> rem3 @ i, (i=0) -> r, (i=1) -> rem4 @ j] +hedberg (A : U) (a b : A) (h : (x : A) -> stable (Id A a x)) + (p q : Id A a b) : Id (Id A a b) p q = + comp (<_> A) a [ (j = 0) -> rem2 @ i + , (j = 1) -> rem3 @ i + , (i = 0) -> r + , (i = 1) -> rem4 @ j] where - ra : Id A a a = refl A a - rem1 (x:A) : exConst (Id A a x) = stableConst (Id A a x) (h x) - f (x:A) : Id A a x -> Id A a x = (rem1 x).1 + ra : Id A a a = <_> a + rem1 (x : A) : exConst (Id A a x) = stableConst (Id A a x) (h x) + f (x : A) : Id A a x -> Id A a x = (rem1 x).1 fIsConst (x : A) : const (Id A a x) (f x) = (rem1 x).2 rem4 : Square A a a ra b b (refl A b) (f b p) (f b q) = fIsConst b p q r : Id A a a = f a ra @@ -20,15 +25,7 @@ hedberg (A:U) (a b:A) (h: (x:A) -> stable (Id A a x)) (p q : Id A a b) : Id (Id rem3 : Square A a a ra a b q r (f b q) = hedbergLemma A a b f q hedbergS (A:U) (h : (a x:A) -> stable (Id A a x)) : set A = - \ (a b:A) -> hedberg A a b (h a) + \(a b : A) -> hedberg A a b (h a) -{- normal form - \(A : U) -> - \(h : (a x : A) -> (((IdP ( A) a x) -> N0) -> N0) -> (IdP ( A) a x)) -> - \(a b : A) -> - \(p q : IdP ( A) a b) -> - comp A a [ (!0 = 0) -> comp A (comp A (h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ !2) [ (!2 = 1) -> p @ (!3 /\ !1) ]) [ (!1 = 1) -> comp A (h a (p @ !3) (\(h0 : (IdP ( A) a (p @ !3)) -> N0) -> h0 ( p @ (!3 /\ !1))) @ !2) [ (!2 = 1) -> p @ (!3 \/ !4) ] ], (!0 = 1) -> comp A (comp A (h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ !2) [ (!2 = 1) -> q @ (!3 /\ !1) ]) [ (!1 = 1) -> comp A (h a (q @ !3) (\(h0 : (IdP ( A) a (q @ !3)) -> N0) -> h0 ( q @ (!3 /\ !1))) @ !2) [ (!2 = 1) -> q @ (!3 \/ !4) ] ], (!1 = 0) -> h a a (\(h0 : (IdP ( A) a a) -> N0) -> h0 ( a)) @ !2, (!1 = 1) -> h a b (\(x : (IdP ( A) a b) -> N0) -> efq (IdP ( N0) (x p) (x q)) (x p) @ !0) @ !2 ] --} - -corrhedberg (A:U) (h : discrete A) : set A = - \ (a b :A) -> hedberg A a b (\ (b:A) -> decStable (Id A a b) (h a b)) \ No newline at end of file +corrhedberg (A : U) (h : discrete A) : set A = + \(a b : A) -> hedberg A a b (\(b : A) -> decStable (Id A a b) (h a b)) \ No newline at end of file -- 2.34.1