Less definitional equalities for glue

diff --git a/Eval.hs b/Eval.hs
index 3c157c8b3f96f8e9feef18da6582ca67be69798f..66c7778a79e0d0ba1133715fe9fd98b474fb2b8e 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -468,18 +468,15 @@ eqToIso e = VPair e1 (VPair f (VPair g (VPair s t)))
         t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv
 
 glue :: Val -> System Val -> Val
-glue b ts | Map.null ts         = b
-          | eps `Map.member` ts = hisoDom (ts ! eps)
+glue b ts | eps `Map.member` ts = hisoDom (ts ! eps)
           | otherwise           = VGlue b ts
 
 glueElem :: Val -> System Val -> Val
-glueElem v us | Map.null us         = v
-              | eps `Map.member` us = us ! eps
+glueElem v us | eps `Map.member` us = us ! eps
               | otherwise           = VGlueElem v us
 
 unGlue :: Val -> Val -> System Val -> Val
 unGlue w b hisos
-    | Map.null hisos         = w
     | eps `Map.member` hisos = app (hisoFun (hisos ! eps)) w
     | otherwise              = case w of
        VGlueElem v us   -> v

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index 09e88848d6aafe0f958182ac2e4621c0db7de4de..ecaebd579740ce6248aa41442b401a1f314c9782 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -86,12 +86,32 @@ kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
 --                      (k = 0)  -> p,
 --                      (k = 1)  -> s @ j ]
 
+idfun (A : U) (a : A) : A = a
+
 isoId (A B : U) (f : A -> B) (g : B -> A)
       (s : (y:B) -> Id B (f (g y)) y)
       (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
-      <i> glue B [ (i = 0) -> (A,f,g,s,t) ]
+      <i> glue A [ (i=0) -> (A,idfun A,idfun A,refl A,refl A), (i = 1) -> (B,g,f,t,s) ]
 
-idfun (A : U) (a : A) : A = a
+isoId' (A B : U) (f : A -> B) (g : B -> A)
+      (s : (y:B) -> Id B (f (g y)) y)
+      (t : (x:A) -> Id A (g (f x)) x) : Id U A B =
+ <i> glue A
+       [ (i = 1) -> (B,g,f,t,s)
+       , (i = 0) ->
+           (A
+           ,\ (x : A) -> comp (<_> A) x [  ]
+           ,\ (y : A) -> comp (<_> A) y [  ]
+           ,\ (y : A) -> <i> comp (<_> A) (comp (<_> A) y [  ])
+                              [ (i = 0) -> <j> comp (<_> A) (comp (<_> A) y [  ])
+                                 [ (j = 0) -> <_> comp (<_> A) y [  ] ]
+                              , (i = 1) -> <j> comp (<_> A) y [ (j = 1) -> <_> y ]
+                              ]
+           ,\ (x : A) -> <i> comp (<_> A) (comp (<_> A) x [  ])
+                              [ (i = 0) -> <j> comp (<_> A) (comp (<_> A) x [  ])
+                                 [ (j = 0) -> <_> comp (<_> A) x [  ] ]
+                              , (i = 1) -> <j> comp (<_> A) x [ (j = 1) -> <_> x ] ])
+       ]
 
 -- isoIdRef (A : U) :
 --   Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) =