From 4a79ca0d64630932ecc0b22a712a36059eaa3a11 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Mon, 15 Jun 2015 14:51:25 +0200 Subject: [PATCH] Finished eqToEquiv --- Eval.hs | 79 ++++++++++++++++++++++++++++++++++++-------- examples/prelude.ctt | 59 ++++++++++++++++++--------------- 2 files changed, 99 insertions(+), 39 deletions(-) diff --git a/Eval.hs b/Eval.hs index 67fe378..7103af6 100644 --- a/Eval.hs +++ b/Eval.hs @@ -358,7 +358,7 @@ 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) + VU -> glue u (Map.map (eqToEquiv . VPath i) ts) VGlue b equivs -> 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 @@ -439,10 +439,45 @@ equivFun x = -- TODO: adapt to equivs -- Every path in the universe induces an hiso -eqToIso :: Val -> Val -eqToIso e = VPair e1 (VPair f (VPair g (VPair s t))) +-- 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) empty +-- -- eplus : e0 -> e1 +-- eplus z = Comp ev z Map.empty +-- -- eminus : e1 -> e0 +-- eminus z = Comp evinv z Map.empty +-- -- NB: edown is *not* transNegFill +-- eup z = Fill ev z Map.empty +-- edown z = Fill evinv z Map.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 b is a four-tuple (a,f,s,t) where +-- a : U +-- f : a -> b +-- s : (y : b) -> fiber a b f y +-- t : (y : b) (w : fiber a b f y) -> s y = w +-- with fiber a b f y = (x : a) * (f x = y) + + +-- Every path in the universe induces an equivalence +eqToEquiv :: Val -> Val +eqToEquiv e = VPair e1 (VPair f (VPair s t)) where e1 = e @@ One - (i,j,x,y,ev) = (Name "i",Name "j",Var "x",Var "y",Var "E") + (i,j,k,x,y,w,ev) = (Name "i",Name "j",Name "k",Var "x",Var "y",Var "w",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) @@ -455,15 +490,33 @@ eqToIso e = VPair e1 (VPair f (VPair g (VPair s t))) eup z = Fill ev z Map.empty edown z = Fill evinv z Map.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 + -- 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 `Map.member` ts = equivDom (ts ! eps) diff --git a/examples/prelude.ctt b/examples/prelude.ctt index 986081c..705e3ff 100644 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@ -96,30 +96,30 @@ lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c) idfun (A : U) (a : A) : A = a -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 A [ (i=0) -> (A,idfun A,idfun A,refl A,refl A), (i = 1) -> (B,g,f,t,s) ] - -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 A - [ (i = 1) -> (B,g,f,t,s) - , (i = 0) -> - (A - ,\ (x : A) -> comp (<_> A) x [ ] - ,\ (y : A) -> comp (<_> A) y [ ] - ,\ (y : A) -> comp (<_> A) (comp (<_> A) y [ ]) - [ (i = 0) -> comp (<_> A) (comp (<_> A) y [ ]) - [ (j = 0) -> <_> comp (<_> A) y [ ] ] - , (i = 1) -> comp (<_> A) y [ (j = 1) -> <_> y ] - ] - ,\ (x : A) -> comp (<_> A) (comp (<_> A) x [ ]) - [ (i = 0) -> comp (<_> A) (comp (<_> A) x [ ]) - [ (j = 0) -> <_> comp (<_> A) x [ ] ] - , (i = 1) -> comp (<_> A) x [ (j = 1) -> <_> x ] ]) - ] +-- 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 A [ (i=0) -> (A,idfun A,idfun A,refl A,refl A), (i = 1) -> (B,g,f,t,s) ] + +-- 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 A +-- [ (i = 1) -> (B,g,f,t,s) +-- , (i = 0) -> +-- (A +-- ,\ (x : A) -> comp (<_> A) x [ ] +-- ,\ (y : A) -> comp (<_> A) y [ ] +-- ,\ (y : A) -> comp (<_> A) (comp (<_> A) y [ ]) +-- [ (i = 0) -> comp (<_> A) (comp (<_> A) y [ ]) +-- [ (j = 0) -> <_> comp (<_> A) y [ ] ] +-- , (i = 1) -> comp (<_> A) y [ (j = 1) -> <_> y ] +-- ] +-- ,\ (x : A) -> comp (<_> A) (comp (<_> A) x [ ]) +-- [ (i = 0) -> comp (<_> A) (comp (<_> A) x [ ]) +-- [ (j = 0) -> <_> comp (<_> A) x [ ] ] +-- , (i = 1) -> comp (<_> A) x [ (j = 1) -> <_> x ] ]) +-- ] -- isoIdRef (A : U) : -- Id (Id U A A) (refl U A) (isoId A A (idfun A) (idfun A) (refl A) (refl A)) = @@ -169,10 +169,17 @@ propPi (A : U) (B : A -> U) (h : (x : A) -> prop (B x)) IdS (A : U) (P : A -> U) (a0 a1 : A) (p : Id A a0 a1) (u0 : P a0) (u1 : P a1) : U = IdP ( P (p @ i)) u0 u1 + +lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a :A) : + (a1 : A) (p : Id A a a1) (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1 = + J A a (\ (a1 : A) (p : Id A a a1) -> (b0 : P a) (b1 : P a1) -> IdP (P (p@i)) b0 b1) rem + where rem : (b0 b1:P a) -> Id (P a) b0 b1 = pP a + + -- lemPropF (A : U) (P : A -> U) (pP : (x : A) -> prop (P x)) (a0 a1 : A) -- (p : Id A a0 a1) (b0 : P a0) (b1 : P a1) : IdS A P a0 a1 p b0 b1 = --- (pP (p @ i) (transport ( P (p @ i /\ j)) b0) --- (transport ( P (p @ i \/ -j)) b1)) @ i +-- (pP (p @ i) (comp ( P (p @ i /\ j)) b0 [ ]) +-- (comp ( P (p @ i \/ -j)) b1 [])) @ i -- Basic data types -- 2.34.1