From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 8 Jan 2016 09:54:54 +0000 (+0100)
Subject: cleaning
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=b57c59f02bcef4e229b75c6e147f741e464b7675;p=cubicaltt.git

cleaning
---

diff --git a/Eval.hs b/Eval.hs
index 8705205..aa009f2 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -585,24 +585,20 @@ pathComp i a u0 u' us = VPath j $ comp i a u0 us'
 -------------------------------------------------------------------------------
 -- | Composition in the Universe
 
-unGlueU :: Val -> Val -> System Val -> Val
-unGlueU w b es
-    | eps `Map.member` es = transNegLine (es ! eps) w
-    | otherwise           = case w of
-       VGlueElem v us   -> v
-       _ -> VUnGlueElemU w b es
+-- any path between types define an equivalence
+eqFun :: Val -> Val -> Val
+eqFun = transNegLine
 
+unGlueU :: Val -> Val -> System Val -> Val
+unGlueU w b es | eps `Map.member` es = eqFun (es ! eps) w
+               | otherwise           = case w of
+                                        VGlueElem v us   -> v
+                                        _ -> VUnGlueElemU w b es
 
 compUniv :: Val -> System Val -> Val
 compUniv b es | eps `Map.member` es = (es ! eps) @@ One
               | otherwise           = VCompU b es
 
--- any path between types define an equivalence
-
-eqFun :: Val -> Val -> Val
-eqFun e t = transNeg i (e @@ i) t
- where i = fresh (e,t)
-
 compU :: Name -> Val -> System Val -> Val -> System Val -> Val
 compU i a eqs wi0 ws = glueElem vi1' usi1
   where ai1 = a `face` (i ~> 1)
@@ -829,8 +825,7 @@ instance Convertible Val where
       (VHComp a u ts,VHComp a' u' ts')    -> conv ns (a,u,ts) (a',u',ts')
       (VGlue v equivs,VGlue v' equivs')   -> conv ns (v,equivs) (v',equivs')
       (VGlueElem u us,VGlueElem u' us')   -> conv ns (u,us) (u',us')
-      -- Anders: these two are from the compU branch:
-      (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'  -- ??
+      (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'  -- Is this correct?
       (VUnGlueElem u ts,VUnGlueElem u' ts') -> conv ns (u,ts) (u',ts')
       (VCompU u es,VCompU u' es')              -> conv ns (u,es) (u',es')
       _                                        -> False