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
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
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
(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
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)
projects / cubicaltt.git / commitdiff