Add genComp and some examples for debugging

diff --git a/Eval.hs b/Eval.hs
index f7547d4f02ccec44d92801603c5087a39d0a5a51..3144eefdd010cfe1271f97c1143c5db33ae378e4 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -333,10 +333,12 @@ fillLine :: Val -> Val -> System Val -> Val
 fillLine a u ts = VPath i $ fill i (a @@ i) u (Map.map (@@ i) ts)
   where i = fresh (a,u,ts)
 
-fill, fillNeg :: Name -> Val -> Val -> System Val -> Val
+fill :: Name -> Val -> Val -> System Val -> Val
 fill i a u ts =
   comp j (a `conj` (i,j)) u (insertSystem (i ~> 0) u (ts `conj` (i,j)))
   where j = fresh (Atom i,a,u,ts)
+
+fillNeg :: Name -> Val -> Val -> System Val -> Val
 fillNeg i a u ts = (fill i (a `sym` i) u (ts `sym` i)) `sym` i
 
 comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]

diff --git a/Exp.cf b/Exp.cf
index 0b5e55bfa7055111b05baa0028e5b6fd94e7e14a..0c0dcf3ef9cf6f1e622000d89d054afab4d5b181 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -33,6 +33,7 @@ App.          Exp2 ::= Exp2 Exp3 ;
 IdP.          Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
 Trans.        Exp3 ::= "transport" Exp4 Exp4 ;
 Comp.         Exp3 ::= "comp" Exp4 Exp4 System ;
+GenComp.      Exp3 ::= "genComp" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "glue" Exp4 System ;
 -- GlueElem.     Exp3 ::= "glueElem" Exp4 System ;
 -- CompElem.     Exp3 ::= "compElem" Exp4 System Exp4 System ;

diff --git a/Resolver.hs b/Resolver.hs
index 16d70c72c1479b61f95a2e0244b02dfb41809ad1..60c9ebc7c41ca75e9f3986d19e5f3352f16d1f0c 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -206,6 +206,9 @@ resolveExp e = case e of
   IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
   Comp u v ts -> CTT.Comp <$> (CTT.Path (C.Name "_") <$> resolveExp u)
                    <*> resolveExp v <*> resolveSystem ts
+
+  GenComp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+
   Glue u ts   -> do
     rs <- resolveSystem ts
     let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True

diff --git a/examples/booltest.ctt b/examples/booltest.ctt
new file mode 100644 (file)
index 0000000..3d20e99
--- /dev/null
+++ b/examples/booltest.ctt
@@ -0,0 +1,32 @@
+module booltest where
+
+import bool
+import newhedberg
+
+falseNotTrue (h : Id bool false true) : N0 = transport (<i> T (h @ i)) tt
+  where T : bool -> U = split
+    false -> Unit
+    true  -> N0
+
+trueNotFalse (h : Id bool true false) : N0 = falseNotTrue (<i> h @ - i)
+
+lemFalse : (b : bool) -> dec (Id bool false b) = split
+  false -> inl (<i> false)
+  true -> inr falseNotTrue
+
+lemTrue : (b : bool) -> dec (Id bool true b) = split
+  false -> inr trueNotFalse
+  true -> inl (<i> true)
+
+boolDec : (a b : bool) -> dec (Id bool a b) = split
+  false -> lemFalse
+  true -> lemTrue
+
+boolSet : set bool = corrhedberg bool boolDec
+
+F2Set : set F2 = subst U set bool F2 boolEqF2 boolSet
+
+T : U = Id F2 oneF2 oneF2
+p0 : T = refl F2 oneF2
+
+test : Id T p0 p0 = F2Set oneF2 oneF2 p0 p0
\ No newline at end of file

diff --git a/examples/integer.ctt b/examples/integer.ctt
index 332d99437d5b7a7779602fde713cb3a5f39c511e..8caa322aad6d38780067102d1cde0a21aca6f94b 100644 (file)
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -58,8 +58,14 @@ T : U = Id int (pos zero) (pos zero)
 p0 : T = refl int (pos zero)
 p1 : T = compId int (pos zero) (neg zero) (pos zero) zeroP' (<i>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))
 test1 : Id T p0 p1 = intSet (pos zero) (pos zero) p0 p1
+test2 : Id T p0 p0 = intSet (pos zero) (pos zero) p0 p0
 
+test3 : Id T p0 p1 = <i1 i2> comp (int) (comp (int) (comp (int) (pos zero) [ (i1 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i1 = 1) -> <i3> comp (int) (comp (int) (comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ] ], (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp (int) (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]
+
+--test3 : Id T p0 p0 = <i1 i2> comp (int) (comp (int) (comp (int) (pos zero) [ (i1 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i1 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp (int) (pos zero) [ (i2 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 0) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp (int) (comp (int) (comp (int) (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> comp (int) (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp (int) (comp (int) (pos zero) [  ]) [ (i3 = 0) -> <i3> comp (int) (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> pos zero, (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> pos zero, (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]
 
 -- test2 : Id T p0 p1 =
 --  <i j> comp int (pos zero)
@@ -72,4 +78,6 @@ test1 : Id T p0 p1 = intSet (pos zero) (pos zero) p0 p1
 --                                                           [ (m = 1) -> <n> comp int (zeroP {int} @ j)
 --                                                                    [ (j = 1) -> <p> zeroP {int} @ (-n \/ -p) ] ])
 --                                                [ (j = 1) -> <n> comp int (zeroP {int} @ (-n /\ m))
---                                                                    [ (m = 1) -> <p> zeroP {int} @ (-n /\ -p) ] ]]]]
\ No newline at end of file
+--                                                                    [ (m = 1) -> <p> zeroP {int} @ (-n /\ -p) ] ]]]]
+
+-- test2 : Id T p0 p1 = <i1 i2> comp int (comp int (comp int (pos zero) [ (i1 = 0) -> <i3> comp int (comp int (comp int (pos zero) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i1 = 1) -> <i3> comp int (comp int (comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ]) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp int (pos zero) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ]) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ]) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero, (i3 = 0) -> <i3> comp int (comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ]) [ (i2 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ], (i2 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ] ] ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ] ], (i2 = 0) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ], (i2 = 1) -> <i3> comp int (comp int (comp int (pos zero) [  ]) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> comp int (pos zero) [ (i3 = 0) -> <i3> pos zero, (i3 = 1) -> <i3> comp int (comp int (pos zero) [  ]) [ (i3 = 0) -> <i3> comp int (pos zero) [  ] ] ], (i3 = 1) -> <i3> pos zero ], (i3 = 1) -> <i3> pos zero ] ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]) [ (i1 = 0) -> <i3> pos zero, (i1 = 1) -> <i3> comp int (zeroP {int} @ i2) [ (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> zeroP {int} @ -i3 ], (i2 = 0) -> <i3> pos zero, (i2 = 1) -> <i3> pos zero ]

diff --git a/examples/interval.ctt b/examples/interval.ctt
index 813a881ff34bf86dd57914cb1859f167ab5d593f..36dc6ae54d90a1a75350d791214c4dd0d193d1e5 100644 (file)
--- a/examples/interval.ctt
+++ b/examples/interval.ctt
@@ -11,3 +11,73 @@ fext (A B : U) (f g : A -> B) (p : (x : A) -> Id B (f x) (g x)) :
           zero    -> f x
           one     -> g x
           seg @ i -> p x @ i
+
+
+toUnit : I -> Unit = split
+  zero -> tt
+  one  -> tt
+  seg @ i -> tt
+
+fromUnit : Unit -> I = split
+  tt -> zero
+
+toUnitK : (a : Unit) -> Id Unit (toUnit (fromUnit a)) a = split
+  tt -> <i> tt
+
+fromUnitK : (a : I) -> Id I (fromUnit (toUnit a)) a = split
+  zero -> <i> zero
+  one -> <i> seg {I} @ i
+  seg @ i -> <j> seg {I} @ i /\ j
+
+unitEqI : Id U Unit I = isoId Unit I fromUnit toUnit fromUnitK toUnitK
+
+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) -> <i> x)
+test2 : T = fooI zero
+
+-- ntest2 : T = <i1> comp I (comp I (comp I zero [ (i1 = 0) -> <i2> comp I (comp I (comp I zero [  ]) [  ]) [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> zero, (i2 = 1) -> <i2> comp I (comp I zero [  ]) [ (i2 = 0) -> <i2> comp I zero [  ] ] ], (i2 = 1) -> <i2> zero ], (i2 = 1) -> <i2> zero ], (i1 = 1) -> <i2> comp I (comp I (comp I zero [  ]) [  ]) [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> zero, (i2 = 1) -> <i2> comp I (comp I zero [  ]) [ (i2 = 0) -> <i2> comp I zero [  ] ] ], (i2 = 1) -> <i2> zero ], (i2 = 1) -> <i2> zero ] ]) [ (i1 = 0) -> <i2> zero, (i1 = 1) -> <i2> zero ]) [ (i1 = 0) -> <i2> zero, (i1 = 1) -> <i2> zero ]
+
+-- test1 : T = <i1> comp I (comp I (comp I zero [ (i1 = 0) -> <i2> comp I (comp I (comp I zero [  ]) [  ]) [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> zero, (i2 = 1) -> <i2> comp I (comp I zero [  ]) [ (i2 = 0) -> <i2> comp I zero [  ] ] ], (i2 = 1) -> <i2> zero ], (i2 = 1) -> <i2> zero ], (i1 = 1) -> <i2> comp I (comp I (comp I zero [  ]) [  ]) [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> comp I zero [ (i2 = 0) -> <i2> zero, (i2 = 1) -> <i2> comp I (comp I zero [  ]) [ (i2 = 0) -> <i2> comp I zero [  ] ] ], (i2 = 1) -> <i2> zero ], (i2 = 1) -> <i2> zero ] ]) [ (i1 = 0) -> <i2> zero, (i1 = 1) -> <i2> zero ]) [ (i1 = 0) -> <i2> zero, (i1 = 1) -> <i2> zero ]
+
+
+-- [ (i2 = 0) -> <i2> zero
+-- , (i2 = 1) -> <i2> comp (<_> I) (comp (<_> I) zero [])
+--                                 [ (i2 = 0) -> <i2> comp (<_> I) zero []]]
+
+-- with zero
+
+
+test : Unit = transport (<i> unitEqI @ -i) zero
+test' : IdP (<i> unitEqI @ -i) zero tt =
+  <i> genComp (<k> unitEqI @ -i \/ -k) zero [(i = 0) -> <_> zero]
+
+test'' : Id I zero zero = <i0> comp I
+             (comp I
+               (comp I zero [ (i0 = 0) -> <i1> zero ])
+                 [ (i0 = 0) -> <i1> zero ])
+             [ (i0 = 0) -> <i1> zero, (i0 = 1) -> <i1> comp I zero [ (i1 = 0) -> <i1> comp I zero [ (i1 = 0) -> <i1> zero, (i1 = 1) -> <i1> comp I (comp I zero [  ]) [ (i1 = 0) -> <i1> comp I zero [  ] ] ], (i1 = 1) -> <i1> zero ] ]
+
+-- -- <i0> glueElem
+--            (comp I
+--              (comp I
+--                (comp I zero [ (i0 = 0) -> <i1> zero ])
+--                  [ (i0 = 0) -> <i1> zero ])
+--              [ (i0 = 0) -> <i1> zero, (i0 = 1) -> <i1> comp I zero [ (i1 = 0) -> <i1> comp I zero [ (i1 = 0) -> <i1> zero, (i1 = 1) -> <i1> comp I (comp I zero [  ]) [ (i1 = 0) -> <i1> comp I zero [  ] ] ], (i1 = 1) -> <i1> zero ] ])
+--            [ (i0 = 1) -> tt ]
+
+-- test : I = transport unitEqI tt
+-- eqttzero : IdP unitEqI tt zero =
+--   <i> genComp (<j> unitEqI @ -i \/ -j) zero [(i=1) -> <_>zero]
+--  <i> transport (<j> unitEqI @ -i \/ -j) zero
+--  <i> genComp (<j> unitEqI @ i /\ j) tt [(i=0) -> tt]
+
+-- Type checking failed: path endpoints don't match for comp (<j> unitEqI @ (i /\ j)) tt [  ], got (tt,comp I (comp I (comp I zero [  ]) [  ]) [  ]), but expected (tt,zero)