Switched back to equiv, simplified glue

diff --git a/Eval.hs b/Eval.hs
index 8659638a9f9c4bd5e173cc35972ee34e5bf302cd..09d7d893801e355b75f1fc7ec12d0dbae79651a5 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -278,8 +278,8 @@ comp i a u ts = case a of
           ui1        = comp i a u1 t1s
           comp_u2    = comp i (app f fill_u1) u2 t2s
   VPi{} -> VComp (VPath i a) u (Map.map (VPath i) ts)
-  VU    -> glue u (Map.map (eqToIso . VPath i) ts)
-  VGlue b isos | not (isNeutralGlue i isos u ts) -> compGlue i b isos u ts
+  VU    -> glue u (Map.map (eqToEquiv . VPath i) ts)
+  VGlue b equivs | not (isNeutralGlue i equivs u ts) -> compGlue i b equivs u ts
   Ter (Sum _ _ nass) env -> case u of
     VCon n us | all isCon (elems ts) -> case lookupLabel n nass of
       Just as -> let tsus = transposeSystemAndList (Map.map unCon ts) us
@@ -439,59 +439,69 @@ hComp a u us | eps `member` us = (us ! eps) @@ One
 
 -------------------------------------------------------------------------------
 -- | Glue
---
--- An iso 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
-
--- Extraction functions for getting a, f, g, s and t:
-isoDom :: Val -> Val
-isoDom = fstVal
-
-isoFun :: Val -> Val
-isoFun = fstVal . sndVal
-
-isoInv :: Val -> Val
-isoInv = fstVal . sndVal . sndVal
-
-isoSec :: Val -> Val
-isoSec = fstVal . sndVal . sndVal . sndVal
-
-isoRet :: Val -> Val
-isoRet = sndVal . sndVal . sndVal . sndVal
-
--- -- Every path in the universe induces an iso
-eqToIso :: Val -> Val
-eqToIso e = VPair e1 (VPair f (VPair g (VPair s t)))
-  where e1 = e @@ One
-        (i,j,x,y,ev) = (Name "i",Name "j",Var "x",Var "y",Var "E")
-        inv t = Path i $ AppFormula t (NegAtom i)
-        evinv = inv ev
-        (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) -- (b,a)
-        eenv     = upd ("E",e) emptyEnv
-        -- eplus : e0 -> e1
-        eplus z  = Comp ev z empty
-        -- eminus : e1 -> e0
-        eminus z = Comp evinv z empty
-        -- NB: edown is *not* transNegFill
-        eup z   = Fill ev z empty
-        edown z = Fill evinv z empty
-        f = Ter (Lam "x" ev1 (eminus x)) eenv
-        g = Ter (Lam "y" ev0 (eplus y)) eenv
-        -- s : (y : e0) -> eminus (eplus y) = y
-        ssys = mkSystem [(j ~> 1, inv (eup y))
-                        ,(j ~> 0, edown (eplus y))]
-        s = Ter (Lam "y" ev0 $ Path j $ Comp evinv (eplus y) ssys) eenv
-        -- t : (x : e1) -> eplus (eminus x) = x
-        tsys = mkSystem [(j ~> 0, eup (eminus x))
-                        ,(j ~> 1, inv (edown x))]
-        t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv
+
+-- An equivalence for a type a is a triple (t,f,p) where
+-- t : U
+-- f : t -> a
+-- p : (x : a) -> isContr ((y:t) * Id a x (f y))
+-- with isContr c = (z : c) * ((z' : C) -> Id c z z')
+
+-- Extraction functions for getting a, f, s and t:
+equivDom :: Val -> Val
+equivDom = fstVal
+
+equivFun :: Val -> Val
+equivFun = fstVal . sndVal
+
+equivContr :: Val -> Val
+equivContr =  sndVal . sndVal
+
+-- Every path in the universe induces an equivalence
+eqToEquiv :: Val -> Val
+eqToEquiv e = undefined -- VPair e1 (VPair f (VPair s t))
+  -- where (i,j,x,y,w,ev) = (Name "i",Name "j",Var "x",Var "y",Var "w",Var "E")
+  --       e1    = e @@ One
+  --       inv t = Path i $ AppFormula t (NegAtom i)
+  --       evinv = inv ev
+  --       (ev0,ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One)) -- (b,a)
+  --       eenv     = upd ("E",e) emptyEnv
+  --       -- eplus : e0 -> e1
+  --       eplus z  = Comp ev z empty
+  --       -- eminus : e1 -> e0
+  --       eminus z = Comp evinv z empty
+  --       -- NB: edown is *not* transNegFill
+  --       eup z   = Fill ev z empty
+  --       edown z = Fill evinv z empty
+  --       f = Ter (Lam "x" ev1 (eminus x)) eenv
+  --       -- g = Ter (Lam "y" ev0 (eplus y)) eenv
+  --       etasys z0 = mkSystem [(j ~> 1, inv (eup z0))
+  --                            ,(j ~> 0, edown (eplus z0))]
+  --       -- eta : (y : e0) -> eminus (eplus y) = y
+  --       eta z0 = Path j $ Comp evinv (eplus z0) (etasys z0)
+  --       etaSquare z0 = Fill evinv (eplus z0) (etasys z0)
+  --       s = Ter (Lam "y" ev0 $ Pair (eplus y) (eta y)) eenv
+  --       (a,p) = (Fst w,Snd w) -- a : e1 and p : eminus a = y
+  --       phisys l = mkSystem [ (l ~> 0, inv (edown a))
+  --                           , (l ~> 1, eup y)]
+  --       psi l = Comp ev (AppFormula p (Atom l)) (phisys l)
+  --       phi l = Fill ev (AppFormula p (Atom l)) (phisys l)
+  --       tsys = mkSystem
+  --                [ (j ~> 0, edown (psi i))
+  --                , (j ~> 1, inv $ eup y)
+  --                , (i ~> 0, inv $ phi j)
+  --                , (i ~> 1, etaSquare y) ]
+  --       -- encode act on terms using Path and AppFormula
+  --       psi' formula = AppFormula (Path j $ psi j) formula
+  --       tprinc = psi' (Atom i :\/: Atom j)
+  --       t2 = Comp evinv tprinc tsys
+  --       t2inv = AppFormula (inv (Path i t2)) (Atom i)
+  --       fibtype = Sigma (Lam "x" ev1 $ IdP (Path (Name "_") ev0) (eminus x) y)
+  --       t = Ter (Lam "y" ev0 $ Lam "w" fibtype $ Path i $
+  --                Pair (psi' (NegAtom i)) (Path j t2inv)) eenv
+
 
 glue :: Val -> System Val -> Val
-glue b ts | eps `member` ts = isoDom (ts ! eps)
+glue b ts | eps `member` ts = equivDom (ts ! eps)
           | otherwise       = VGlue b ts
 
 glueElem :: Val -> System Val -> Val
@@ -499,68 +509,83 @@ glueElem v us | eps `member` us = us ! eps
               | otherwise       = VGlueElem v us
 
 unGlue :: Val -> Val -> System Val -> Val
-unGlue w b isos | eps `member` isos = app (isoFun (isos ! eps)) w
-                | otherwise         = case w of
-                                        VGlueElem v us -> v
-                                        _ -> error ("unGlue: neutral" ++ show w)
+unGlue w b equivs | eps `member` equivs = app (equivFun (equivs ! eps)) w
+                  | otherwise           = case w of
+                                            VGlueElem v us -> v
+                                            _ -> error ("unGlue: neutral" ++ show w)
 
 isNeutralGlue :: Name -> System Val -> Val -> System Val -> Bool
-isNeutralGlue i isos u0 ts = (eps `notMember` isosi0 && isNeutral u0) ||
+isNeutralGlue i equivs u0 ts = (eps `notMember` equivsi0 && isNeutral u0) ||
   any (\(alpha,talpha) ->
-           eps `notMember` (isos `face` alpha) && isNeutral talpha)
+           eps `notMember` (equivs `face` alpha) && isNeutral talpha)
     (assocs ts)
-  where isosi0 = isos `face` (i ~> 0)
-
+  where equivsi0 = equivs `face` (i ~> 0)
+
+
+-- Extend the system ts to a total element in b given q : isContr b
+extend :: Val -> Val -> System Val -> Val
+extend b q ts = comp i b (fstVal q) ts'
+  where i = fresh (b,q,ts)
+        ts' = mapWithKey
+                (\alpha tAlpha -> app ((sndVal q) `face` alpha) tAlpha @@@ i) ts
+
+-- psi/b corresponds to ws
+-- b0    corresponds to wi0
+-- a0    corresponds to vi0
+-- psi/a corresponds to vs
+-- a1'   corresponds to vi1'
+-- equivs' corresponds to delta
+-- ti1'  corresponds to usi1'
 compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val
-compGlue i b isos wi0 ws = glueElem vi1'' usi1''
-  where bi1 = b `face` (i ~> 1)
-        vs   = mapWithKey
-                 (\alpha wAlpha -> unGlue wAlpha
-                                     (b `face` alpha) (isos `face` alpha)) ws
+compGlue i a equivs wi0 ws = glueElem vi1' usi1
+  where ai1 = a `face` (i ~> 1)
+        vs  = mapWithKey
+                (\alpha wAlpha ->
+                  unGlue wAlpha (a `face` alpha) (equivs `face` alpha)) ws
+
         vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs
-        vi0  = unGlue wi0 (b `face` (i ~> 0)) (isos `face` (i ~> 0)) -- in b(i0)
+        vi0  = unGlue wi0 (a `face` (i ~> 0)) (equivs `face` (i ~> 0)) -- in a(i0)
 
-        v    = fill i b vi0 vs           -- in b
-        vi1  = comp i b vi0 vs           -- is v `face` (i ~> 1) in b(i1)
+        vi1'  = comp i a vi0 vs           -- in a(i1)
 
-        isosI1 = isos `face` (i ~> 1)
-        isos'  = filterWithKey (\alpha _ -> i `notMember` alpha) isos
-        isos'' = filterWithKey (\alpha _ -> alpha `notMember` isos) isosI1
+        equivsI1 = equivs `face` (i ~> 1)
+        equivs'  = filterWithKey (\alpha _ -> i `notMember` alpha) equivs
 
-        us'    = mapWithKey (\gamma isoG ->
-                   fill i (isoDom isoG) (wi0 `face` gamma) (ws `face` gamma))
-                 isos'
-        usi1'  = mapWithKey (\gamma isoG ->
-                   comp i (isoDom isoG) (wi0 `face` gamma) (ws `face` gamma))
-                 isos'
+        us'    = mapWithKey (\gamma equivG ->
+                   fill i (equivDom equivG) (wi0 `face` gamma) (ws `face` gamma))
+                 equivs'
+        usi1'  = mapWithKey (\gamma equivG ->
+                   comp i (equivDom equivG) (wi0 `face` gamma) (ws `face` gamma))
+                 equivs'
 
-        ls'    = mapWithKey (\gamma isoG ->
-                   pathComp i (b `face` gamma) (vi0 `face` gamma)
-                     (isoFun isoG `app` (us' ! gamma)) (vs `face` gamma))
-                 isos'
+        -- path in ai1 between vi1 and f(i1) usi1' on equivs'
+        ls'    = mapWithKey (\gamma equivG ->
+                   pathComp i (a `face` gamma) (vi0 `face` gamma)
+                     (equivFun equivG `app` (us' ! gamma)) (vs `face` gamma))
+                 equivs'
 
-        vi1' = compLine (constPath bi1) vi1
-                 (ls' `unionSystem` Map.map constPath vsi1)
+        fibersys = intersectionWith VPair usi1' ls' -- on equivs'
 
         wsi1 = ws `face` (i ~> 1)
-
-        -- for gamma in isos'', (i1) gamma is in isos, so wsi1 gamma
-        -- is in the domain of isoGamma
-        uls'' = mapWithKey (\gamma isoG ->
-                  gradLemma (bi1 `face` gamma) isoG
-                    ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma))
-                    (vi1' `face` gamma))
-                  isos''
-
-        vsi1' = Map.map constPath $ border vi1' isos' `unionSystem` vsi1
-
-        vi1'' = compLine (constPath bi1) vi1'
-                  (Map.map snd uls'' `unionSystem` vsi1')
-
-        usi1'' = mapWithKey (\gamma _ ->
-                     if gamma `member` usi1' then usi1' ! gamma
-                     else fst (uls'' ! gamma))
-                   isosI1
+        fibersys' = mapWithKey
+          (\gamma equivG ->
+            let fibsgamma = intersectionWith (\ x y -> VPair x (constPath y))
+                              (wsi1 `face` gamma) (vsi1 `face` gamma)
+            in extend (mkFiberType (ai1 `face` gamma) (vi1' `face` gamma) equivG)
+                 (equivContr equivG)
+                 (fibsgamma `unionSystem` (fibersys `face` gamma))) equivsI1
+
+        vi1 = compLine (constPath ai1) vi1'
+                  (Map.map sndVal fibersys')
+
+        usi1 = Map.map fstVal fibersys'
+
+mkFiberType :: Val -> Val -> Val -> Val
+mkFiberType a x equiv = eval rho $
+  Sigma $ Lam "y" tt (IdP (Path (Name "_") ta) tx (App tf ty))
+  where [ta,tx,ty,tf,tt] = map Var ["a","x","y","f","t"]
+        rho = upds [("a",a),("x",x),("f",equivFun equiv)
+                   ,("t",equivDom equiv)] emptyEnv
 
 -- Assumes u' : A is a solution of us + (i0 -> u0)
 -- The output is an L-path in A(i1) between comp i u0 us and u'(i1)
@@ -569,30 +594,30 @@ pathComp i a u0 u' us = VPath j $ comp i a u0 us'
   where j   = fresh (Atom i,a,us,u0,u')
         us' = insertsSystem [(j ~> 1, u')] us
 
--- Grad Lemma, takes an iso f, a system us and a value v, s.t. f us =
--- border v. Outputs (u,p) s.t. border u = us and a path p between v
--- and f u.
-gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
-gradLemma b iso us v = (u, VPath i theta'')
-  where i:j:_   = freshs (b,iso,us,v)
-        (a,f,g,s,t) = (isoDom iso,isoFun iso,isoInv iso,isoSec iso,isoRet iso)
-        us'     = mapWithKey (\alpha uAlpha ->
-                                   app (t `face` alpha) uAlpha @@@ i) us
-        gv      = app g v
-        theta   = fill i a gv us'
-        u       = comp i a gv us'  -- Same as "theta `face` (i ~> 1)"
-        ws      = insertSystem (i ~> 0) gv $
-                  insertSystem (i ~> 1) (app t u @@@ j) $
-                  mapWithKey
-                    (\alpha uAlpha ->
-                      app (t `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us
-        theta'  = compNeg j a theta ws
-        xs      = insertSystem (i ~> 0) (app s v @@@ j) $
-                  insertSystem (i ~> 1) (app s (app f u) @@@ j) $
-                  mapWithKey
-                    (\alpha uAlpha ->
-                      app (s `face` alpha) (app (f `face` alpha) uAlpha) @@@ j) us
-        theta'' = comp j b (app f theta') xs
+-- -- Grad Lemma, takes an iso f, a system us and a value v, s.t. f us =
+-- -- border v. Outputs (u,p) s.t. border u = us and a path p between v
+-- -- and f u.
+-- gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
+-- gradLemma b iso us v = (u, VPath i theta'')
+--   where i:j:_   = freshs (b,iso,us,v)
+--         (a,f,g,s,t) = (isoDom iso,isoFun iso,isoInv iso,isoSec iso,isoRet iso)
+--         us'     = mapWithKey (\alpha uAlpha ->
+--                                    app (t `face` alpha) uAlpha @@@ i) us
+--         gv      = app g v
+--         theta   = fill i a gv us'
+--         u       = comp i a gv us'  -- Same as "theta `face` (i ~> 1)"
+--         ws      = insertSystem (i ~> 0) gv $
+--                   insertSystem (i ~> 1) (app t u @@@ j) $
+--                   mapWithKey
+--                     (\alpha uAlpha ->
+--                       app (t `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us
+--         theta'  = compNeg j a theta ws
+--         xs      = insertSystem (i ~> 0) (app s v @@@ j) $
+--                   insertSystem (i ~> 1) (app s (app f u) @@@ j) $
+--                   mapWithKey
+--                     (\alpha uAlpha ->
+--                       app (s `face` alpha) (app (f `face` alpha) uAlpha) @@@ j) us
+--         theta'' = comp j b (app f theta') xs
 
 -------------------------------------------------------------------------------
 -- | Conversion
@@ -647,12 +672,12 @@ instance Convertible Val where
       (VPath i a,VPath i' a')    -> conv ns (a `swap` (i,j)) (a' `swap` (i',j))
       (VPath i a,p')             -> conv ns (a `swap` (i,j)) (p' @@@ j)
       (p,VPath i' a')            -> conv ns (p @@@ j) (a' `swap` (i',j))
-      (VAppFormula u x,VAppFormula u' x')    -> conv ns (u,x) (u',x')
-      (VComp a u ts,VComp a' u' ts')         -> conv ns (a,u,ts) (a',u',ts')
-      (VHComp a u ts,VHComp a' u' ts')       -> conv ns (a,u,ts) (a',u',ts')
-      (VGlue v isos,VGlue v' isos')          -> conv ns (v,isos) (v',isos')
-      (VGlueElem u us,VGlueElem u' us')      -> conv ns (u,us) (u',us')
-      _                                      -> False
+      (VAppFormula u x,VAppFormula u' x') -> conv ns (u,x) (u',x')
+      (VComp a u ts,VComp a' u' ts')      -> conv ns (a,u,ts) (a',u',ts')
+      (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')
+      _                                   -> False
 
 instance Convertible Ctxt where
   conv _ _ _ = True
@@ -706,7 +731,7 @@ instance Normal Val where
     VPath i u           -> VPath i (normal ns u)
     VComp u v vs        -> compLine (normal ns u) (normal ns v) (normal ns vs)
     VHComp u v vs       -> hComp (normal ns u) (normal ns v) (normal ns vs)
-    VGlue u isos        -> glue (normal ns u) (normal ns isos)
+    VGlue u equivs      -> glue (normal ns u) (normal ns equivs)
     VGlueElem u us      -> glueElem (normal ns u) (normal ns us)
     VVar x t            -> VVar x t -- (normal ns t)
     VFst t              -> fstVal (normal ns t)

diff --git a/TypeChecker.hs b/TypeChecker.hs
index a342b0749c9e047efa2dd76b2a9781c82b0be09c..0197e5fb4a687143846277c95617822da7e73385 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -263,17 +263,17 @@ checkGlueElem vu ts us = do
     (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us))\r
   rho <- asks env\r
   checkSystemsWith ts us\r
-    (\alpha vt u -> local (faceEnv alpha) $ check (isoDom vt) u)\r
+    (\alpha vt u -> local (faceEnv alpha) $ check (equivDom vt) u)\r
   let vus = evalSystem rho us\r
   checkSystemsWith ts vus (\alpha vt vAlpha ->\r
-    unlessM (app (isoFun vt) vAlpha === (vu `face` alpha)) $\r
+    unlessM (app (equivFun vt) vAlpha === (vu `face` alpha)) $\r
       throwError $ "Image of glueElem component " ++ show vAlpha ++\r
                    " doesn't match " ++ show vu)\r
   checkCompSystem vus\r
 \r
 checkGlue :: Val -> System Ter -> Typing ()\r
 checkGlue va ts = do\r
-  checkSystemWith ts (\alpha tAlpha -> checkIso (va `face` alpha) tAlpha)\r
+  checkSystemWith ts (\alpha tAlpha -> checkEquiv (va `face` alpha) tAlpha)\r
   rho <- asks env\r
   checkCompSystem (evalSystem rho ts)\r
 \r
@@ -293,8 +293,25 @@ mkIso vb = eval rho $
   where [a,b,f,g,x,y] = map Var ["a","b","f","g","x","y"]\r
         rho = upd ("b",vb) emptyEnv\r
 \r
-checkIso :: Val -> Ter -> Typing ()\r
-checkIso vb iso = check (mkIso vb) iso\r
+-- An equivalence for a type a is a triple (t,f,p) where\r
+-- t : U\r
+-- f : t -> a\r
+-- p : (x : a) -> isContr ((y:t) * Id a x (f y))\r
+-- with isContr c = (z : c) * ((z' : C) -> Id c z z')\r
+mkEquiv :: Val -> Val\r
+mkEquiv va = eval rho $\r
+  Sigma $ Lam "t" U $\r
+  Sigma $ Lam "f" (Pi (Lam "_" t a)) $\r
+  Pi (Lam "x" a $ iscontrfib)\r
+  where [a,b,f,x,y,s,t,z] = map Var ["a","b","f","x","y","s","t","z"]\r
+        rho = upd ("a",va) emptyEnv\r
+        fib = Sigma $ Lam "y" t (IdP (Path (Name "_") a) x (App f y))\r
+        iscontrfib = Sigma $ Lam "s" fib $\r
+                     Pi $ Lam "z" fib $ IdP (Path (Name "_") fib) s z\r
+\r
+checkEquiv :: Val -> Ter -> Typing ()\r
+checkEquiv va equiv = check (mkEquiv va) equiv\r
+\r
 \r
 checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()\r
 checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do\r

diff --git a/examples/prelude.ctt b/examples/prelude.ctt
index da8bf9b775aa6ba2d735aebff31bc0d16c4df020..e0aac1087c34621b698d0f4e7a45c626caac4a6d 100644 (file)
--- a/examples/prelude.ctt
+++ b/examples/prelude.ctt
@@ -238,8 +238,23 @@ injective (A B : U) (f : A -> B) : U =
 and (A B : U) : U = (_ : A) * B
 
 
-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 = 1) -> (B,idfun B,idfun B,refl B,refl B) ]
+-- 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 = 1) -> (B,idfun B,idfun B,refl B,refl B) ]
+
+fiber (A B : U) (f : A -> B) (y : B) : U =
+  (x : A) * Id B y (f x)
+
+isEquiv (A B : U) (f : A -> B) : U =
+  (y : B) -> isContr (fiber A B f y)
+
+idIsEquiv (A : U) : isEquiv A A (idfun A) =
+  \ (a : A) ->
+  ((a, refl A a)
+  , \ (z : fiber A A (idfun A) a) -> contrSingl A a z.1 z.2)
+
+
+equivId (T A : U) (f : T -> A) (p : isEquiv T A f) : Id U T A =
+  <i> glue A [ (i=0) -> (T,f,p), (i=1) -> (A,idfun A, idIsEquiv A)]