Fix a bug in eqLemma

diff --git a/Eval.hs b/Eval.hs
index 62f5345258aada447c9b2f74a2de7c60d8944626..fc8b0bd32cc1244b313b876ea812abe15f6ac42f 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -609,6 +609,7 @@ transU i a es wi0 =
 
       ls' = mapWithKey (\gamma _ ->
               pathUnivTrans i (es `proj` gamma) (wi0 `face` gamma))
+--                         pathUniv i (es `proj` gamma) Map.empty (wi0 `face` gamma))
             es'
 
       vi1' = compLine ai1 vi1 ls'
@@ -638,13 +639,13 @@ eqLemma e ts a = (t,VPath j theta'')
   where i:j:_   = freshs (e,ts,a)
         ei      = e @@ i
         vs      = mapWithKey (\alpha uAlpha ->
-                    transFill i (ei `face` alpha) uAlpha) ts
-        theta   = genFillNeg i ei a vs
-        t       = genCompNeg i ei a vs
-        theta'  = transFill i ei t
+                    transFillNeg i (ei `face` alpha) uAlpha) ts
+        theta   = genFill i ei a vs
+        t       = genComp i ei a vs
+        theta'  = transFillNeg i ei t
         ws      = insertSystem (j ~> 1) theta' $
                   insertSystem (j ~> 0) theta $ vs
-        theta'' = genComp i ei t ws
+        theta'' = genCompNeg i ei t ws
 
 
 -------------------------------------------------------------------------------

diff --git a/examples/circle.ctt b/examples/circle.ctt
index 6e68af356f36cdc6c2c866623c191c4c1156bc12..be59ff2a0b2954b1032f1d297f3429899068031c 100644 (file)
--- a/examples/circle.ctt
+++ b/examples/circle.ctt
@@ -23,4 +23,7 @@ winding (p : loopS1) : Z = transport rem zeroZ
 
 loop2 : loopS1 = compId S1 base base base loop' loop'
 loop2' : loopS1 = compId' S1 base base base loop' loop'
-loop2'' : loopS1 = compId'' S1 base base loop' base loop'
\ No newline at end of file
+loop2'' : loopS1 = compId'' S1 base base loop' base loop'
+
+
+test : Id U Z Z = compId U Z Z Z sucIdZ sucIdZ 
\ No newline at end of file