From: Anders Mörtberg Date: Thu, 31 Dec 2015 07:54:15 +0000 (+0100) Subject: Merge branch 'compU' X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=877c83ddfb78f28c27556f0c0c35d53b81425df7;p=cubicaltt.git Merge branch 'compU' # Conflicts: # CTT.hs # Eval.hs # examples/testEquiv.ctt --- 877c83ddfb78f28c27556f0c0c35d53b81425df7 diff --cc CTT.hs index 885f5df,5166b33..0b0d88a --- a/CTT.hs +++ b/CTT.hs @@@ -146,13 -145,10 +146,11 @@@ data Val = V -- Glue values | VGlue Val (System Val) | VGlueElem Val (System Val) + | VUnGlueElem Val (System Val) -- -- Composition in the universe (for now) ++ -- Composition in the universe | VCompU Val (System Val) - - -- Composition for HITs; the type is constant | VHComp Val Val (System Val) diff --cc Eval.hs index 862e0af,e49c229..6afdc2c --- a/Eval.hs +++ b/Eval.hs @@@ -480,104 -505,101 +480,105 @@@ glueElem (VUnGlueElem u _) _ = glueElem v us | eps `member` us = us ! eps | otherwise = VGlueElem v us +unglueElem :: Val -> System Val -> Val +unglueElem w isos | eps `member` isos = app (equivFun (isos ! eps)) w + | otherwise = case w of + VGlueElem v us -> v + _ -> VUnGlueElem w isos + 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) ++-- this is exactly the same as isNeutralGlue? +isNeutralU :: Name -> System Val -> Val -> System Val -> Bool +isNeutralU i eqs u0 ts = (eps `notMember` eqsi0 && isNeutral u0) || + any (\(alpha,talpha) -> + eps `notMember` (eqs `face` alpha) && isNeutral talpha) + (assocs ts) + where eqsi0 = eqs `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) (v `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 - --- assumes u and u' : A are solutions of us + (i0 -> u(i0)) --- The output is an L-path in A(i1) between u(i1) and u'(i1) + 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) + (app (equivContr equivG) (vi1' `face` gamma)) + (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) pathComp :: Name -> Val -> Val -> Val -> System Val -> Val -pathComp i a u u' us = VPath j $ comp i a (u `face` (i ~> 0)) us' - where j = fresh (Atom i,a,us,u,u') - us' = insertsSystem [(j ~> 0, u), (j ~> 1, u')] us +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 ------------------------------------------------------------------------------- -- | Composition in the Universe @@@ -589,127 -611,59 +590,129 @@@ unGlueU w b e VGlueElem v us -> v _ -> VUnGlueElemU w b es ++ compUniv :: Val -> System Val -> Val compUniv b es | eps `Map.member` es = (es ! eps) @@ One | otherwise = VCompU b es -compU :: Name -> Val -> System Val -> Val -> System Val -> Val -compU i b es wi0 ws = glueElem vi1'' usi1'' - where bi1 = b `face` (i ~> 1) - vs = mapWithKey (\alpha wAlpha -> - unGlueU wAlpha (b `face` alpha) (es `face` alpha)) ws - vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs - vi0 = unGlueU wi0 (b `face` (i ~> 0)) (es `face` (i ~> 0)) -- in b(i0) +-- any path between types define an equivalence - v = fill i b vi0 vs -- in b - vi1 = comp i b vi0 vs -- is v `face` (i ~> 1) in b(i1) +eqFun :: Val -> Val -> Val +eqFun e t = transNeg i (e @@ i) t + where i = fresh (e,t) - esI1 = es `face` (i ~> 1) - es' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es - es'' = filterWithKey (\alpha _ -> alpha `Map.notMember` es) esI1 - - us' = mapWithKey (\gamma eGamma -> - fill i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma)) - es' - usi1' = mapWithKey (\gamma eGamma -> - comp i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma)) - es' ++compU :: Name -> Val -> System Val -> Val -> System Val -> Val +compU i a eqs wi0 ws = glueElem vi1' usi1 + where ai1 = a `face` (i ~> 1) + vs = mapWithKey + (\alpha wAlpha -> + unGlueU wAlpha (a `face` alpha) (eqs `face` alpha)) ws - ls' = mapWithKey (\gamma eGamma -> - pathComp i (b `face` gamma) (v `face` gamma) - (transNegLine eGamma (us' ! gamma)) (vs `face` gamma)) - es' + vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs + vi0 = unGlueU wi0 (a `face` (i ~> 0)) (eqs `face` (i ~> 0)) -- in a(i0) - vi1' = compLine (constPath bi1) vi1 - (ls' `unionSystem` Map.map constPath vsi1) + vi1' = comp i a vi0 vs -- in a(i1) - wsi1 = ws `face` (i ~> 1) + eqsI1 = eqs `face` (i ~> 1) + eqs' = filterWithKey (\alpha _ -> i `notMember` alpha) eqs - -- for gamma in es'', (i1) gamma is in es, so wsi1 gamma - -- is in the domain of isoGamma - uls'' = mapWithKey (\gamma eGamma -> - gradLemmaU (bi1 `face` gamma) eGamma - ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma)) - (vi1' `face` gamma)) - es'' + us' = mapWithKey (\gamma eqG -> + fill i (eqG @@ One) (wi0 `face` gamma) (ws `face` gamma)) + eqs' + usi1' = mapWithKey (\gamma eqG -> + comp i (eqG @@ One) (wi0 `face` gamma) (ws `face` gamma)) + eqs' - vsi1' = Map.map constPath $ border vi1' es' `unionSystem` vsi1 + -- path in ai1 between vi1 and f(i1) usi1' on equivs' + ls' = mapWithKey (\gamma eqG -> + pathComp i (a `face` gamma) (vi0 `face` gamma) + (eqFun eqG (us' ! gamma)) (vs `face` gamma)) + eqs' - vi1'' = compLine (constPath bi1) vi1' - (Map.map snd uls'' `unionSystem` vsi1') + fibersys = intersectionWith (\ x y -> (x,y)) usi1' ls' -- on eqs' - usi1'' = Map.mapWithKey (\gamma _ -> - if gamma `Map.member` usi1' then usi1' ! gamma - else fst (uls'' ! gamma)) - esI1 + wsi1 = ws `face` (i ~> 1) + fibersys' = mapWithKey + (\gamma eqG -> + let fibsgamma = intersectionWith (\ x y -> (x,constPath y)) + (wsi1 `face` gamma) (vsi1 `face` gamma) + in lemEq eqG (vi1' `face` gamma) (fibsgamma `unionSystem` (fibersys `face` gamma))) eqsI1 + + vi1 = compLine (constPath ai1) vi1' (Map.map snd fibersys') + + usi1 = Map.map fst fibersys' + + +lemEq :: Val -> Val -> System (Val,Val) -> (Val,Val) +lemEq eq b aps = (a,VPath i (compNeg j (eq @@ j) p1 ths)) + where + ths = insertsSystem [(i ~> 0,transFill j eq b),(i ~> 1,transFillNeg j eq a)] thetas + i:j:_ = freshs (eq,b,aps) + ta = eq @@ One + eqi = eq @@ i + a = comp i ta (trans i eqi b) p1s + p1 = fill i ta (trans i eqi b) p1s + thetas = mapWithKey (\alpha (aa,pa) -> + let eqaj = (eq `face` alpha) @@ j + ba = b `face` alpha + in fill j eqaj (pa @@ i) + (mkSystem [ (i~>0,transFill j eqaj ba),(i~>1,transFillNeg j eqaj aa)])) aps + p1s = mapWithKey (\alpha (aa,pa) -> + let eqaj = (eq `face` alpha) @@ j + ba = b `face` alpha + in comp j eqaj (pa @@ i) + (mkSystem [ (i~>0,transFill j eqaj ba),(i~>1,transFillNeg j eqaj aa)])) aps + - ++-- Old version: +-- compU :: Name -> Val -> System Val -> Val -> System Val -> Val +-- compU i b es wi0 ws = glueElem vi1'' usi1'' +-- where bi1 = b `face` (i ~> 1) +-- vs = mapWithKey (\alpha wAlpha -> +-- unGlueU wAlpha (b `face` alpha) (es `face` alpha)) ws +-- vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs +-- vi0 = unGlueU wi0 (b `face` (i ~> 0)) (es `face` (i ~> 0)) -- in b(i0) + +-- v = fill i b vi0 vs -- in b +-- vi1 = comp i b vi0 vs -- is v `face` (i ~> 1) in b(i1) + +-- esI1 = es `face` (i ~> 1) +-- es' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) es +-- es'' = filterWithKey (\alpha _ -> alpha `Map.notMember` es) esI1 + +-- us' = mapWithKey (\gamma eGamma -> +-- fill i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma)) +-- es' +-- usi1' = mapWithKey (\gamma eGamma -> +-- comp i (eGamma @@ One) (wi0 `face` gamma) (ws `face` gamma)) +-- es' + +-- ls' = mapWithKey (\gamma eGamma -> +-- pathComp i (b `face` gamma) (v `face` gamma) +-- (transNegLine eGamma (us' ! gamma)) (vs `face` gamma)) +-- es' + +-- vi1' = compLine (constPath bi1) vi1 +-- (ls' `unionSystem` Map.map constPath vsi1) + +-- wsi1 = ws `face` (i ~> 1) + +-- -- for gamma in es'', (i1) gamma is in es, so wsi1 gamma +-- -- is in the domain of isoGamma +-- uls'' = mapWithKey (\gamma eGamma -> +-- gradLemmaU (bi1 `face` gamma) eGamma +-- ((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma)) +-- (vi1' `face` gamma)) +-- es'' + +-- vsi1' = Map.map constPath $ border vi1' es' `unionSystem` vsi1 + +-- vi1'' = compLine (constPath bi1) vi1' +-- (Map.map snd uls'' `unionSystem` vsi1') + +-- usi1'' = Map.mapWithKey (\gamma _ -> +-- if gamma `Map.member` usi1' then usi1' ! gamma +-- else fst (uls'' ! gamma)) +-- esI1 -- Grad Lemma, takes a line eq in U, 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 @@@ -727,8 -681,41 +730,42 @@@ gradLemmaU b eq us v = (u, VPath i thet insertSystem (i ~> 1) (transFillNeg j ej u) $ ws theta = compNeg j ej u xs -{- -gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val) -gradLemmaU b eq us v = (u, VPath i theta'') - where i:j:_ = freshs (b,eq,us,v) - a = eq @@ One - g = transLine - f = transNegLine - s e y = VPath j $ compNeg i (e @@ i) (trans i (e @@ i) y) - (mkSystem [(j ~> 0, transFill j (e @@ j) y) - ,(j ~> 1, transFillNeg j (e @@ j) - (trans j (e @@ j) y))]) - t e x = VPath j $ comp i (e @@ i) (transNeg i (e @@ i) x) - (mkSystem [(j ~> 0, transFill j (e @@ j) - (transNeg j (e @@ j) x)) - ,(j ~> 1, transFillNeg j (e @@ j) x)]) - gv = g eq v - us' = mapWithKey (\alpha uAlpha -> - t (eq `face` alpha) uAlpha @@ i) us - 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) (t eq u @@ j) $ - mapWithKey - (\alpha uAlpha -> - t (eq `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us - theta' = compNeg j a theta ws - xs = insertSystem (i ~> 0) (s eq v @@ j) $ - insertSystem (i ~> 1) (s eq (f eq u) @@ j) $ - mapWithKey - (\alpha uAlpha -> - s (eq `face` alpha) (f (eq `face` alpha) uAlpha) @@ j) us - theta'' = comp j b (f eq theta') xs --} + + ++-- Old version: ++-- gradLemmaU :: Val -> Val -> System Val -> Val -> (Val, Val) ++-- gradLemmaU b eq us v = (u, VPath i theta'') ++-- where i:j:_ = freshs (b,eq,us,v) ++-- a = eq @@ One ++-- g = transLine ++-- f = transNegLine ++-- s e y = VPath j $ compNeg i (e @@ i) (trans i (e @@ i) y) ++-- (mkSystem [(j ~> 0, transFill j (e @@ j) y) ++-- ,(j ~> 1, transFillNeg j (e @@ j) ++-- (trans j (e @@ j) y))]) ++-- t e x = VPath j $ comp i (e @@ i) (transNeg i (e @@ i) x) ++-- (mkSystem [(j ~> 0, transFill j (e @@ j) ++-- (transNeg j (e @@ j) x)) ++-- ,(j ~> 1, transFillNeg j (e @@ j) x)]) ++-- gv = g eq v ++-- us' = mapWithKey (\alpha uAlpha -> ++-- t (eq `face` alpha) uAlpha @@ i) us ++-- 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) (t eq u @@ j) $ ++-- mapWithKey ++-- (\alpha uAlpha -> ++-- t (eq `face` alpha) uAlpha @@ (Atom i :/\: Atom j)) us ++-- theta' = compNeg j a theta ws ++-- xs = insertSystem (i ~> 0) (s eq v @@ j) $ ++-- insertSystem (i ~> 1) (s eq (f eq u) @@ j) $ ++-- mapWithKey ++-- (\alpha uAlpha -> ++-- s (eq `face` alpha) (f (eq `face` alpha) uAlpha) @@ j) us ++-- theta'' = comp j b (f eq theta') xs + + ------------------------------------------------------------------------------- -- | Conversion @@@ -780,14 -767,16 +817,17 @@@ instance Convertible Val wher (VVar x _, VVar x' _) -> x == x' (VIdP a b c,VIdP a' b' c') -> conv ns a a' && conv ns b b' && conv ns c c' (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') + (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 equivs,VGlue v' equivs') -> conv ns (v,equivs) (v',equivs') + (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') - _ -> False ++ -- Anders: these two are from the compU branch: + (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u' - (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') - _ -> False ++ (VCompU u es,VCompU u' es') -> conv ns (u,es) (u',es') ++ _ -> False instance Convertible Ctxt where conv _ _ _ = True @@@ -841,11 -830,8 +881,13 @@@ instance Normal Val wher 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) + VUnGlueElem u us -> unglueElem (normal ns u) (normal ns us) + VUnGlueElemU e u us -> unGlueU (normal ns e) (normal ns u) (normal ns us) + VCompU a ts -> VCompU (normal ns a) (normal ns ts) ++ -- TODO: Shouldn't we do: ++ -- VCompU u es -> compUniv (normal ns u) (normal ns es) VVar x t -> VVar x t -- (normal ns t) VFst t -> fstVal (normal ns t) VSnd t -> sndVal (normal ns t) diff --cc examples/prelude.ctt index 076a6d1,20d5b43..26779a5 --- a/examples/prelude.ctt +++ b/examples/prelude.ctt @@@ -237,82 -241,9 +241,84 @@@ injective (A B : U) (f : A -> B) : U and (A B : U) : U = (_ : A) * B + propAnd (A B : U) (pA : prop A) (pB : prop B) : prop (and A B) = + propSig A (\(_ : A) -> B) pA (\(_ : A) -> pB) +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)] + + + +--- isoId + +lemIso (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) + (y : B) (x0 x1 : A) (p0 : Id B y (f x0)) (p1 : Id B y (f x1)) : + Id (fiber A B f y) (x0,p0) (x1,p1) = (p @ i,sq1 @ i) + where + rem0 : Id A (g y) x0 = + comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0, (i = 0) -> <_> g y ] + + rem1 : Id A (g y) x1 = + comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1, (i = 0) -> <_> g y ] + + p : Id A x0 x1 = + comp (<_> A) (g y) [ (i = 0) -> rem0 + , (i = 1) -> rem1 ] + + fill0 : Square A (g y) (g (f x0)) (g y) x0 + ( g (p0 @ i)) rem0 ( g y) (t x0) = + comp (<_> A) (g (p0 @ i)) [ (i = 1) -> t x0 @ j /\ k + , (i = 0) -> <_> g y + , (j = 0) -> <_> g (p0 @ i) ] + + fill1 : Square A (g y) (g (f x1)) (g y) x1 + ( g (p1 @ i)) rem1 ( g y) (t x1) = + comp (<_> A) (g (p1 @ i)) [ (i = 1) -> t x1 @ j /\ k + , (i = 0) -> <_> g y + , (j = 0) -> <_> g (p1 @ i) ] + + fill2 : Square A (g y) (g y) x0 x1 + (<_> g y) p rem0 rem1 = + comp (<_> A) (g y) [ (i = 0) -> rem0 @ j /\ k + , (i = 1) -> rem1 @ j /\ k + , (j = 0) -> <_> g y ] + + sq : Square A (g y) (g y) (g (f x0)) (g (f x1)) + ( g y) ( g (f (p @ i))) + ( g (p0 @ j)) ( g (p1 @ j)) = + comp (<_> A) (fill2 @ i @ j) [ (i = 0) -> fill0 @ j @ -k + , (i = 1) -> fill1 @ j @ -k + , (j = 0) -> <_> g y + , (j = 1) -> t (p @ i) @ -k ] + + sq1 : Square B y y (f x0) (f x1) + (<_>y) ( f (p @ i)) p0 p1 = + comp (<_> B) (f (sq @ i @j)) [ (i = 0) -> s (p0 @ j) + , (i = 1) -> s (p1 @ j) + , (j = 1) -> s (f (p @ i)) + , (j = 0) -> s y ] + +gradLemma (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) : isEquiv A B f = + \ (y:B) -> ((g y,s y@-i),\ (z:fiber A B f y) -> lemIso A B f g s t y (g y) z.1 (s y@-i) z.2) + + + 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 =