From: Anders <mortberg@chalmers.se>
Date: Thu, 26 Mar 2015 16:41:13 +0000 (+0100)
Subject: Fix a bug in eqLemma
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=7cbfb1de076e49ef4f6032cf2bea0ea4e80be9da;p=cubicaltt.git

Fix a bug in eqLemma
---

diff --git a/Eval.hs b/Eval.hs
index 62f5345..fc8b0bd 100644
--- 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 6e68af3..be59ff2 100644
--- 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