From ba3406ae07c360ece6409b56e72f2f03eaac49ec Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Wed, 16 Dec 2015 12:30:48 +0100 Subject: [PATCH] Switched back to equiv, simplified glue --- Eval.hs | 291 +++++++++++++++++++++++-------------------- TypeChecker.hs | 27 +++- examples/prelude.ctt | 25 +++- 3 files changed, 200 insertions(+), 143 deletions(-) diff --git a/Eval.hs b/Eval.hs index 8659638..09d7d89 100644 --- 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 a342b07..0197e5f 100644 --- 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)) rho <- asks env checkSystemsWith ts us - (\alpha vt u -> local (faceEnv alpha) $ check (isoDom vt) u) + (\alpha vt u -> local (faceEnv alpha) $ check (equivDom vt) u) let vus = evalSystem rho us checkSystemsWith ts vus (\alpha vt vAlpha -> - unlessM (app (isoFun vt) vAlpha === (vu `face` alpha)) $ + unlessM (app (equivFun vt) vAlpha === (vu `face` alpha)) $ throwError $ "Image of glueElem component " ++ show vAlpha ++ " doesn't match " ++ show vu) checkCompSystem vus checkGlue :: Val -> System Ter -> Typing () checkGlue va ts = do - checkSystemWith ts (\alpha tAlpha -> checkIso (va `face` alpha) tAlpha) + checkSystemWith ts (\alpha tAlpha -> checkEquiv (va `face` alpha) tAlpha) rho <- asks env checkCompSystem (evalSystem rho ts) @@ -293,8 +293,25 @@ mkIso vb = eval rho $ where [a,b,f,g,x,y] = map Var ["a","b","f","g","x","y"] rho = upd ("b",vb) emptyEnv -checkIso :: Val -> Ter -> Typing () -checkIso vb iso = check (mkIso vb) iso +-- 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') +mkEquiv :: Val -> Val +mkEquiv va = eval rho $ + Sigma $ Lam "t" U $ + Sigma $ Lam "f" (Pi (Lam "_" t a)) $ + Pi (Lam "x" a $ iscontrfib) + where [a,b,f,x,y,s,t,z] = map Var ["a","b","f","x","y","s","t","z"] + rho = upd ("a",va) emptyEnv + fib = Sigma $ Lam "y" t (IdP (Path (Name "_") a) x (App f y)) + iscontrfib = Sigma $ Lam "s" fib $ + Pi $ Lam "z" fib $ IdP (Path (Name "_") fib) s z + +checkEquiv :: Val -> Ter -> Typing () +checkEquiv va equiv = check (mkEquiv va) equiv + checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing () checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do diff --git a/examples/prelude.ctt b/examples/prelude.ctt index da8bf9b..e0aac10 100644 --- 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 = - 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 = +-- 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 = + glue A [ (i=0) -> (T,f,p), (i=1) -> (A,idfun A, idIsEquiv A)] -- 2.34.1