From: Simon Huber <hubsim@gmail.com>
Date: Fri, 5 Jun 2015 15:54:27 +0000 (+0200)
Subject: Less definitional equalities for glue
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=5ac7a21fce5fcf198720f5ead820a21f3252e6dc;p=cubicaltt.git

Less definitional equalities for glue
---

diff --git a/Eval.hs b/Eval.hs
index 3c157c8..66c7778 100644
--- 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 09e8884..ecaebd5 100644
--- 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)) =