fixed bug; switched a with b in hiso

diff --git a/Eval.hs b/Eval.hs
index 2d99b8b9edbbc1d361278b201fb2a23ac0abfe7c..67b66aa37124f80ca50673f3f936a6f310c4c772 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -6,6 +6,7 @@ import Data.Maybe (fromMaybe)
 import Data.Map (Map,(!))
 import qualified Data.Map as Map
 
+
 import Connections
 import CTT
 
@@ -112,6 +113,7 @@ instance Nominal Val where
          VSplit u v        -> VSplit (sw u) (sw v)
          VGlue a ts        -> VGlue (sw a) (sw ts)
          VGlueElem a ts    -> VGlueElem (sw a) (sw ts)
+
 -----------------------------------------------------------------------
 -- The evaluator
 
@@ -274,18 +276,18 @@ transGlue i b hisos wi0 = glueElem vi1'' usi1
           Map.filterWithKey (\alpha _ -> alpha `Map.notMember` hisos) hisosI1
 
         -- set of elements in hisos independent of i
-        hisos'  = Map.filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos
+        hisos' = Map.filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos
 
-        us'    = Map.mapWithKey (\gamma _ ->
-                  transFill i (b `face` gamma) (wi0 `face` gamma))
+        us'    = Map.mapWithKey (\gamma isoG ->
+                  transFill i (hisoDom isoG) (wi0 `face` gamma))
                  hisos'
-        usi1'  = Map.mapWithKey (\gamma _ ->
-                  trans i (b `face` gamma) (wi0 `face` gamma))
+        usi1'  = Map.mapWithKey (\gamma isoG ->
+                   trans i (hisoDom isoG) (wi0 `face` gamma))
                  hisos'
 
         ls'    = Map.mapWithKey (\gamma isoG ->
-                  pathComp i (hisoDom isoG) (v `face` gamma)
-                           ((hisoFun isoG) `app` (us' ! gamma)) Map.empty)
+                   pathComp i (b `face` gamma) (v `face` gamma)
+                   ((hisoFun isoG) `app` (us' ! gamma)) Map.empty)
                  hisos'
         bi1   = b `face` (i ~> 1)
         vi1'  = compLine bi1 vi1 ls'
@@ -307,7 +309,7 @@ transGlue i b hisos wi0 = glueElem vi1'' usi1
 -- outputs u s.t. border u = us and an L-path between v and sigma u
 -- an theta is a L path if L-border theta is constant
 gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
-gradLemma a hiso@(VPair b (VPair f (VPair g (VPair s t)))) us v = (u, VPath i theta'')
+gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v = (u, VPath i theta'')
   where i:j:_   = freshs (a,hiso,us,v)
         us'     = Map.mapWithKey (\alpha uAlpha ->
                                    app (t `face` alpha) uAlpha @@ i) us
@@ -409,16 +411,16 @@ compGlue i b hisos wi0 ws = glueElem vi1' usi1'
         v    = fill i b vi0 vs           -- in b
         vi1  = comp i b vi0 vs           -- in b
 
-        us'    = Map.mapWithKey (\gamma _ ->
-                   fill i (b `face` gamma) (wi0 `face` gamma) (ws `face` gamma))
+        us'    = Map.mapWithKey (\gamma isoG ->
+                   fill i (hisoDom isoG) (wi0 `face` gamma) (ws `face` gamma))
                  hisos
-        usi1'  = Map.mapWithKey (\gamma _ ->
-                   comp i (b `face` gamma) (wi0 `face` gamma) (ws `face` gamma))
+        usi1'  = Map.mapWithKey (\gamma isoG ->
+                   comp i (hisoDom isoG) (wi0 `face` gamma) (ws `face` gamma))
                  hisos
 
         ls'    = Map.mapWithKey (\gamma isoG ->
-                  pathComp i (hisoDom isoG) (v `face` gamma)
-                             (hisoFun isoG `app` (us' ! gamma)) (vs `face` gamma))
+                   pathComp i isoG (v `face` gamma)
+                   (hisoFun isoG `app` (us' ! gamma)) (vs `face` gamma))
                  hisos
 
         vi1'  = compLine b vi1 ls'
@@ -442,16 +444,16 @@ pathComp i a u u' us = VPath j $ genComp i a (u `face` (i ~> 0)) us'
 
 -------------------------------------------------------------------------------
 -- | Glue
--- 
--- An hiso for a type a is a five-tuple: (b,f,g,r,s)   where
---  b : U
---  f : b -> a
---  g : a -> b
---  s : forall (y : a), f (g y) = y
---  t : forall (x : b), g (f x) = x
+--
+-- An hiso for a type b is a five-tuple: (a,f,g,r,s)   where
+--  a : U
+--  f : a -> b
+--  g : b -> a
+--  s : forall (y : b), f (g y) = y
+--  t : forall (x : a), g (f x) = x
 
 hisoDom :: Val -> Val
-hisoDom (VPair b _) = b
+hisoDom (VPair a _) = a
 hisoDom x           = error $ "HisoDom: Not an hiso: " ++ show x
 
 hisoFun :: Val -> Val

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 24277490b83ce276b33f07d2d8bc2bdba4d12e22..c15c5bd163381b4c6970140cac55aa6c9a23d473 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -198,10 +198,9 @@ checkGlueElem vu ts us = do
   unless (Map.keys ts == Map.keys us)\r
     (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us))\r
   rho <- asks env\r
-  k <- asks index\r
+  k   <- asks index\r
   sequence_ $ Map.elems $ Map.intersectionWithKey\r
     (\alpha vt u -> check (hisoDom vt) u) ts us\r
-    \r
   let vus = evalSystem rho us\r
   sequence_ $ Map.elems $ Map.intersectionWithKey\r
     (\alpha vt vAlpha -> do\r
@@ -220,19 +219,19 @@ checkGlue va ts = do
   unless (isCompSystem k (evalSystem rho ts))\r
     (throwError ("Incompatible system " ++ show ts))\r
 \r
--- An hiso for a type a is a five-tuple: (b,f,g,r,s)   where\r
---  b : U\r
---  f : b -> a\r
---  g : a -> b\r
---  s : forall (y : a), f (g y) = y\r
---  t : forall (x : b), g (f x) = x\r
+-- An hiso for a type b is a five-tuple: (a,f,g,r,s)   where\r
+--  a : U\r
+--  f : a -> b\r
+--  g : b -> a\r
+--  s : forall (y : b), f (g y) = y\r
+--  t : forall (x : a), g (f x) = x\r
 checkIso :: Val -> Ter -> Typing ()\r
-checkIso va (Pair b (Pair f (Pair g (Pair s t)))) = do\r
-  check VU b\r
+checkIso vb (Pair a (Pair f (Pair g (Pair s t)))) = do\r
+  check VU a\r
   rho <- asks env\r
-  let vb = eval rho b\r
-  check (mkFun vb va) f\r
-  check (mkFun va vb) g\r
+  let va = eval rho a\r
+  check (mkFun va vb) f\r
+  check (mkFun vb va) g\r
   let vf = eval rho f\r
       vg = eval rho g\r
   check (mkSection va vb vf vg) s\r
@@ -243,11 +242,11 @@ mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b")))
   where rho = Upd (Upd Empty ("a",va)) ("b",vb)\r
 \r
 mkSection :: Val -> Val -> Val -> Val -> Val\r
-mkSection va _ vf vg =\r
-  VPi va (eval rho (Lam "y" a (IdP (Path (Name "_") a) (App f (App g y)) y)))\r
-  where [a,y,f,g] = map Var ["a","y","f","g"]\r
-        rho = Upd (Upd (Upd Empty ("a",va)) ("f",vf)) ("g",vg)\r
-  \r
+mkSection _ vb vf vg =\r
+  VPi vb (eval rho (Lam "y" b (IdP (Path (Name "_") b) (App f (App g y)) y)))\r
+  where [b,y,f,g] = map Var ["b","y","f","g"]\r
+        rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg)\r
+\r
 checkBranch :: (Tele,Env) -> Val -> Branch -> Typing ()\r
 checkBranch (xas,nu) f (c,(xs,e)) = do\r
   k   <- asks index\r