import Control.Applicative
import Data.List
-import Data.Map (Map,(!),keys)
+import Data.Map (Map,(!),keys,fromList,toList,mapKeys,elems,intersectionWith
+ ,unionWith,singleton,foldWithKey,assocs,mapWithKey
+ ,filterWithKey,member)
import Data.Set (Set,isProperSubsetOf)
import qualified Data.Map as Map
import qualified Data.Set as Set
type Face = Map Name Dir
instance Arbitrary Face where
- arbitrary = Map.fromList <$> arbitrary
+ arbitrary = fromList <$> arbitrary
showFace :: Face -> String
showFace alpha = concat [ "(" ++ show i ++ " = " ++ show d ++ ")"
- | (i,d) <- Map.toList alpha ]
+ | (i,d) <- toList alpha ]
swapFace :: Face -> (Name,Name) -> Face
-swapFace alpha ij = Map.mapKeys (`swapName` ij) alpha
+swapFace alpha ij = mapKeys (`swapName` ij) alpha
-- Check if two faces are compatible
compatible :: Face -> Face -> Bool
-compatible xs ys = and (Map.elems (Map.intersectionWith (==) xs ys))
+compatible xs ys = and (elems (intersectionWith (==) xs ys))
compatibles :: [Face] -> Bool
compatibles [] = True
-- Partial composition operation
meet :: Face -> Face -> Face
-meet = Map.unionWith f
+meet = unionWith f
where f d1 d2 = if d1 == d2 then d1 else error "meet: incompatible faces"
meetMaybe :: Face -> Face -> Maybe Face
incomparables (x:xs) = all (not . (x `comparable`)) xs && incomparables xs
(~>) :: Name -> Dir -> Face
-i ~> d = Map.singleton i d
+i ~> d = singleton i d
eps :: Face
eps = Map.empty
-- phi b = max {alpha : Face | phi alpha = b}
invFormula :: Formula -> Dir -> [Face]
invFormula (Dir b') b = [ eps | b == b' ]
-invFormula (Atom i) b = [ Map.singleton i b ]
-invFormula (NegAtom i) b = [ Map.singleton i (- b) ]
+invFormula (Atom i) b = [ singleton i b ]
+invFormula (NegAtom i) b = [ singleton i (- b) ]
invFormula (phi :/\: psi) Zero = invFormula phi 0 `union` invFormula psi 0
invFormula (phi :/\: psi) One = meets (invFormula phi 1) (invFormula psi 1)
invFormula (phi :\/: psi) b = invFormula (negFormula phi :/\: negFormula psi) (- b)
swap (psi1 :\/: psi2) (i,j) = swap psi1 (i,j) :\/: swap psi2 (i,j)
face :: Nominal a => a -> Face -> a
-face = Map.foldWithKey (\i d a -> act a (i,Dir d))
+face = foldWithKey (\i d a -> act a (i,Dir d))
-- the faces should be incomparable
type System a = Map Face a
| (alpha,u) <- ts ] ++ " ]"
showSystem :: Show a => System a -> String
-showSystem = showListSystem . Map.toList
+showSystem = showListSystem . toList
insertSystem :: Face -> a -> System a -> System a
-insertSystem alpha v ts = case find (comparable alpha) (Map.keys ts) of
+insertSystem alpha v ts = case find (comparable alpha) (keys ts) of
Just beta | alpha `leq` beta -> ts
| otherwise -> Map.insert alpha v (Map.delete beta ts)
Nothing -> Map.insert alpha v ts
mkSystem = flip insertsSystem Map.empty
unionSystem :: System a -> System a -> System a
-unionSystem us vs = insertsSystem (Map.assocs us) vs
+unionSystem us vs = insertsSystem (assocs us) vs
-- TODO: add some checks
-- Now we ensure that the keys are incomparable
instance Nominal a => Nominal (System a) where
- support s = unions (map Map.keys $ Map.keys s)
- `union` support (Map.elems s)
+ support s = unions (map keys $ keys s)
+ `union` support (elems s)
- act s (i, phi) = addAssocs (Map.assocs s)
+ act s (i, phi) = addAssocs (assocs s)
where
addAssocs [] = Map.empty
addAssocs ((alpha,u):alphaus) =
s' (invFormula (face phi beta) d)
Nothing -> insertSystem alpha (act u (i,face phi alpha)) s'
- swap s ij = Map.mapKeys (`swapFace` ij) (Map.map (`swap` ij) s)
+ swap s ij = mapKeys (`swapFace` ij) (Map.map (`swap` ij) s)
-- carve a using the same shape as the system b
border :: Nominal a => a -> System b -> System a
-border v = Map.mapWithKey (const . face v)
+border v = mapWithKey (const . face v)
shape :: System a -> System ()
shape = border ()
arbitraryShape :: [Name] -> Gen (System ())
arbitraryShape supp = do
phi <- sized $ arbFormula supp
- return $ Map.fromList [(face,()) | face <- invFormula phi 0]
+ return $ fromList [(face,()) | face <- invFormula phi 0]
sym :: Nominal a => a -> Name -> a
sym a i = a `act` (i, NegAtom i)
leqSystem :: Face -> System a -> Bool
alpha `leqSystem` us =
- not $ Map.null $ Map.filterWithKey (\beta _ -> alpha `leq` beta) us
+ not $ Map.null $ filterWithKey (\beta _ -> alpha `leq` beta) us
-- assumes alpha <= shape us
proj :: (Nominal a, Show a) => System a -> Face -> a
-proj us alpha | eps `Map.member` usalpha = usalpha ! eps
- | otherwise =
+proj us alpha | eps `member` usalpha = usalpha ! eps
+ | otherwise =
error $ "proj: eps not in " ++ show usalpha ++ "\nwhich is the "
++ show alpha ++ "\nface of " ++ show us
where usalpha = us `face` alpha
import Data.List
import Data.Maybe (fromMaybe)
import Data.Map (Map,(!),mapWithKey,assocs,filterWithKey
- ,elems,intersectionWith,intersection,keys)
+ ,elems,intersectionWith,intersection,keys
+ ,member,notMember,empty)
import qualified Data.Map as Map
import Connections
import CTT
+-----------------------------------------------------------------------
+-- Lookup functions
look :: String -> Env -> Val
look x (Upd y rho,v:vs,fs) | x == y = v
Just (_,t) -> eval r t
Nothing -> look x (rho,vs,fs)
look x (Sub _ rho,vs,_:fs) = look x (rho,vs,fs)
+look x _ = error $ "look: not found " ++ show x
lookType :: String -> Env -> Val
lookType x (Upd y rho,VVar _ a:vs,fs)
Just (a,_) -> eval r a
Nothing -> lookType x (rho,vs,fs)
lookType x (Sub _ rho,vs,_:fs) = lookType x (rho,vs,fs)
+lookType x _ = error $ "lookType: not found " ++ show x
lookName :: Name -> Env -> Formula
--- lookName i Empty = error $ "lookName: not found " ++ show i
lookName i (Upd _ rho,v:vs,fs) = lookName i (rho,vs,fs)
-lookName i (Def _ rho,vs,fs) = lookName i (rho,vs,fs)
+lookName i (Def _ rho,vs,fs) = lookName i (rho,vs,fs)
lookName i (Sub j rho,vs,phi:fs) | i == j = phi
| otherwise = lookName i (rho,vs,fs)
+lookName i _ = error $ "lookName: not found " ++ show i
+
-----------------------------------------------------------------------
-- Nominal instances
Undef{} -> Ter v rho
Hole{} -> Ter v rho
IdP a e0 e1 -> VIdP (eval rho a) (eval rho e0) (eval rho e1)
- Path i t ->
- let j = fresh rho
- in VPath j (eval (sub (i,Atom j) rho) t)
+ Path i t -> let j = fresh rho
+ in VPath j (eval (sub (i,Atom j) rho) t)
AppFormula e phi -> eval rho e @@ evalFormula rho phi
Comp a t0 ts -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts)
Fill a t0 ts -> fillLine (eval rho a) (eval rho t0) (evalSystem rho ts)
GlueElem a ts -> glueElem (eval rho a) (evalSystem rho ts)
_ -> error $ "Cannot evaluate " ++ show v
+evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)]
+evals env bts = [ (b,eval env t) | (b,t) <- bts ]
+
evalFormula :: Env -> Formula -> Formula
evalFormula rho phi = case phi of
Atom i -> lookName i rho
phi1 :\/: phi2 -> evalFormula rho phi1 `orFormula` evalFormula rho phi2
_ -> phi
-evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)]
-evals env bts = [ (b,eval env t) | (b,t) <- bts ]
-
evalSystem :: Env -> System Ter -> System Val
evalSystem rho ts =
let out = concat [ let betas = meetss [ invFormula (lookName i rho) d
_ -> VAppFormula v (toFormula phi)
v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral."
-pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val
-pcon c a@(Ter (HSum _ _ lbls) rho) us phis = case lookupPLabel c lbls of
- Just (tele,is,ts) | eps `Map.member` vs -> vs ! eps
- | otherwise -> VPCon c a us phis
- where rho' = subs (zip is phis) (updsTele tele us rho)
- vs = evalSystem rho' ts
- Nothing -> error "pcon"
-pcon c a us phi = VPCon c a us phi
+
+-------------------------------------------------------------------------------
+-- Composition and filling
+
+comp :: Name -> Val -> Val -> System Val -> Val
+comp i a u ts | eps `member` ts = (ts ! eps) `face` (i ~> 1)
+comp i a u ts = case a of
+ VIdP p v0 v1 -> let j = fresh (Atom i,a,u,ts)
+ in VPath j $ comp i (p @@ j) (u @@ j) $
+ insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts)
+ VSigma a f -> VPair ui1 comp_u2
+ where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts)
+ (u1, u2) = (fstVal u, sndVal u)
+ fill_u1 = fill i a u1 t1s
+ 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 (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
+ Just as -> let tsus = transposeSystemAndList (Map.map unCon ts) us
+ in VCon n $ comps i as env tsus
+ Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
+ _ -> VComp (VPath i a) u (Map.map (VPath i) ts)
+ Ter (HSum _ _ nass) env -> compHIT i a u ts
+ _ -> VComp (VPath i a) u (Map.map (VPath i) ts)
+
+compNeg :: Name -> Val -> Val -> System Val -> Val
+compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i)
+
+compLine :: Val -> Val -> System Val -> Val
+compLine a u ts = comp i (a @@ i) u (Map.map (@@ i) ts)
+ where i = fresh (a,u,ts)
+
+comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
+comps i [] _ [] = []
+comps i ((x,a):as) e ((ts,u):tsus) =
+ let v = fill i (eval e a) u ts
+ vi1 = comp i (eval e a) u ts
+ vs = comps i as (upd (x,v) e) tsus
+ in vi1 : vs
+comps _ _ _ _ = error "comps: different lengths of types and values"
+
+fill :: Name -> Val -> Val -> System Val -> Val
+fill i a u ts =
+ comp j (a `conj` (i,j)) u (insertSystem (i ~> 0) u (ts `conj` (i,j)))
+ where j = fresh (Atom i,a,u,ts)
+
+fillNeg :: Name -> Val -> Val -> System Val -> Val
+fillNeg i a u ts = (fill i (a `sym` i) u (ts `sym` i)) `sym` i
+
+fillLine :: Val -> Val -> System Val -> Val
+fillLine a u ts = VPath i $ fill i (a @@ i) u (Map.map (@@ i) ts)
+ where i = fresh (a,u,ts)
+
+-- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
+-- fills i [] _ [] = []
+-- fills i ((x,a):as) e ((ts,u):tsus) =
+-- let v = fill i (eval e a) ts u
+-- vs = fills i as (Upd e (x,v)) tsus
+-- in v : vs
+-- fills _ _ _ _ = error "fills: different lengths of types and values"
+
-----------------------------------------------------------
--- Transport
+-- Transport and squeeze (defined using comp)
+
+trans :: Name -> Val -> Val -> Val
+trans i v0 v1 = comp i v0 v1 empty
+
+transNeg :: Name -> Val -> Val -> Val
+transNeg i a u = trans i (a `sym` i) u
transLine :: Val -> Val -> Val
transLine u v = trans i (u @@ i) v
transNegLine u v = transNeg i (u @@ i) v
where i = fresh (u,v)
-trans :: Name -> Val -> Val -> Val
-trans i v0 v1 = comp i v0 v1 Map.empty
-
-transNeg :: Name -> Val -> Val -> Val
-transNeg i a u = trans i (a `sym` i) u
-
-transFill, transFillNeg :: Name -> Val -> Val -> Val
-transFill i a u = fill i a u Map.empty
-transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i
-
transps :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val]
transps i [] _ [] = []
transps i ((x,a):as) e (u:us) =
in vi1 : vs
transps _ _ _ _ = error "transps: different lengths of types and values"
+transFill :: Name -> Val -> Val -> Val
+transFill i a u = fill i a u empty
+
+transFillNeg :: Name -> Val -> Val -> Val
+transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i
+
-- Given u of type a "squeeze i a u" connects in the direction i
-- trans i a u(i=0) to u(i=1)
squeeze :: Name -> Val -> Val -> Val
squeeze i a u = comp i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ]
- where j = fresh (Atom i,a,u)
+ where j = fresh (Atom i,a,u)
ui1 = u `face` (i ~> 1)
squeezeFill :: Name -> Val -> Val -> Val
squeezeFill i a u = fill i (a `disj` (i,j)) u $ mkSystem [ (j ~> 1, ui1) ]
- where j = fresh (Atom i,a,u)
+ where j = fresh (Atom i,a,u)
ui1 = u `face` (i ~> 1)
squeezes :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val]
-- squeezeNeg i a u = transNeg j (a `conj` (i,j)) u
-- where j = fresh (Atom i,a,u)
--------------------------------------------------------------------------------
--- Composition
-
-compLine :: Val -> Val -> System Val -> Val
-compLine a u ts = comp i (a @@ i) u (Map.map (@@ i) ts)
- where i = fresh (a,u,ts)
-
-fillLine :: Val -> Val -> System Val -> Val
-fillLine a u ts = VPath i $ fill i (a @@ i) u (Map.map (@@ i) ts)
- where i = fresh (a,u,ts)
-
-fill :: Name -> Val -> Val -> System Val -> Val
-fill i a u ts =
- comp j (a `conj` (i,j)) u (insertSystem (i ~> 0) u (ts `conj` (i,j)))
- where j = fresh (Atom i,a,u,ts)
-
-fillNeg :: Name -> Val -> Val -> System Val -> Val
-fillNeg i a u ts = (fill i (a `sym` i) u (ts `sym` i)) `sym` i
-
-comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
-comps i [] _ [] = []
-comps i ((x,a):as) e ((ts,u):tsus) =
- let v = fill i (eval e a) u ts
- vi1 = comp i (eval e a) u ts
- vs = comps i as (upd (x,v) e) tsus
- in vi1 : vs
-comps _ _ _ _ = error "comps: different lengths of types and values"
-
-comp :: Name -> Val -> Val -> System Val -> Val
-comp i a u ts | eps `Map.member` ts = (ts ! eps) `face` (i ~> 1)
-comp i a u ts = case a of
- VIdP p v0 v1 -> let j = fresh (Atom i,a,u,ts)
- in VPath j $ comp i (p @@ j) (u @@ j) $
- insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts)
- VSigma a f -> VPair ui1 comp_u2
- where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts)
- (u1, u2) = (fstVal u, sndVal u)
- fill_u1 = fill i a u1 t1s
- 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 (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
- Just as -> let tsus = transposeSystemAndList (Map.map unCon ts) us
- in VCon n $ comps i as env tsus
- Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
- _ -> VComp (VPath i a) u (Map.map (VPath i) ts)
- Ter (HSum _ _ nass) env -> compHIT i a u ts
- _ -> VComp (VPath i a) u (Map.map (VPath i) ts)
-
-compNeg :: Name -> Val -> Val -> System Val -> Val
-compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i)
-
--- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
--- fills i [] _ [] = []
--- fills i ((x,a):as) e ((ts,u):tsus) =
--- let v = fill i (eval e a) ts u
--- vs = fills i as (Upd e (x,v)) tsus
--- in v : vs
--- fills _ _ _ _ = error "fills: different lengths of types and values"
-------------------------------------------------------------------------------
--- | HIT
+-- | HITs
+
+pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val
+pcon c a@(Ter (HSum _ _ lbls) rho) us phis = case lookupPLabel c lbls of
+ Just (tele,is,ts) | eps `member` vs -> vs ! eps
+ | otherwise -> VPCon c a us phis
+ where rho' = subs (zip is phis) (updsTele tele us rho)
+ vs = evalSystem rho' ts
+ Nothing -> error "pcon"
+pcon c a us phi = VPCon c a us phi
compHIT :: Name -> Val -> Val -> System Val -> Val
compHIT i a u us
_ -> error $ "squeezeHIT: neutral " ++ show u
hComp :: Val -> Val -> System Val -> Val
-hComp a u us | eps `Map.member` us = (us ! eps) @@ One
- | otherwise = VHComp a u us
+hComp a u us | eps `member` us = (us ! eps) @@ One
+ | otherwise = VHComp a u us
+
-------------------------------------------------------------------------------
-- | Glue
-- t : (y : b) (w : fiber a b f y) -> s y = w
-- with fiber a b f y = (x : a) * (f x = y)
+-- Extraction functions for getting a, f, s and t:
equivDom :: Val -> Val
equivDom = fstVal
-- ,(j ~> 1, inv (edown x))]
-- t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv
--- 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,w,ev) = (Name "i",Name "j",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)
- 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
- 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)
- | otherwise = VGlue b ts
+glue b ts | eps `member` ts = equivDom (ts ! eps)
+ | otherwise = VGlue b ts
glueElem :: Val -> System Val -> Val
-glueElem v us | eps `Map.member` us = us ! eps
- | otherwise = VGlueElem v us
+glueElem v us | eps `member` us = us ! eps
+ | otherwise = VGlueElem v us
unGlue :: Val -> Val -> System Val -> Val
unGlue w b equivs
- | eps `Map.member` equivs = app (equivFun (equivs ! eps)) w
- | otherwise = case w of
- VGlueElem v us -> v
- _ -> VUnGlueElem w b equivs
+ | eps `member` equivs = app (equivFun (equivs ! eps)) w
+ | otherwise = case w of
+ VGlueElem v us -> v
+ _ -> VUnGlueElem w b equivs
compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val
compGlue i b equivs wi0 ws = glueElem vi1'' usi1''
where bi1 = b `face` (i ~> 1)
- vs = mapWithKey
- (\alpha wAlpha -> unGlue wAlpha
- (b `face` alpha) (equivs `face` alpha)) ws
+ vs = mapWithKey (\alpha wAlpha ->
+ unGlue wAlpha (b `face` alpha) (equivs `face` alpha))
+ ws
vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs
vi0 = unGlue wi0 (b `face` (i ~> 0)) (equivs `face` (i ~> 0)) -- in b(i0)
vi1 = comp i b vi0 vs -- is v `face` (i ~> 1) in b(i1)
equivsI1 = equivs `face` (i ~> 1)
- equivs' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) equivs
- equivs'' = filterWithKey (\alpha _ -> alpha `Map.notMember` equivs') equivsI1
+ equivs' = filterWithKey (\alpha _ -> i `notMember` alpha) equivs
+ equivs'' = filterWithKey (\alpha _ -> alpha `notMember` equivs') equivsI1
us' = mapWithKey (\gamma isoG ->
fill i (equivDom isoG) (wi0 `face` gamma) (ws `face` gamma))
gradLemma (bi1 `face` gamma) isoG
((usi1' `face` gamma) `unionSystem` (wsi1 `face` gamma))
(vi1' `face` gamma))
- equivs''
+ equivs''
vsi1' = Map.map constPath $ border vi1' equivs' `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))
- equivsI1
-
+ usi1'' = mapWithKey (\gamma _ ->
+ if gamma `member` usi1'
+ then usi1' ! gamma
+ else fst (uls'' ! gamma))
+ equivsI1
-- 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)
-- L-path p between v and f u.
gradLemma :: Val -> Val -> System Val -> Val -> (Val, Val)
gradLemma b e us v = (u,VPath j $ tau `sym` j)
- where i:j:_ = freshs (b,e,us,v)
+ where i:j:_ = freshs (b,e,us,v)
(a,f,s,t) = (equivDom e,equivFun e,equivCenter e,equivIsCenter e)
- g y = fstVal (app s y) -- g : b -> a
- eta y = sndVal (app s y) -- eta b @ i : f (g b) --> b
- us' = mapWithKey
- (\alpha uAlpha ->
- let fuAlpha = app (f `face` alpha) uAlpha
- in app (app (t `face` alpha) fuAlpha)
- (VPair uAlpha (constPath fuAlpha))) us
+ g y = fstVal (app s y) -- g : b -> a
+ eta y = sndVal (app s y) -- eta b @ i : f (g b) --> b
+ us' = mapWithKey (\alpha uAlpha ->
+ let fuAlpha = app (f `face` alpha) uAlpha
+ in app (app (t `face` alpha) fuAlpha)
+ (VPair uAlpha (constPath fuAlpha)))
+ us
theta = fill i a (g v) (Map.map (fstVal . (@@ i)) us')
- u = theta `face` (i ~> 1)
- vs = insertsSystem
- [(j ~> 0, app f theta),(j ~> 1, v)]
- (Map.map ((@@ j) . sndVal . (@@ i)) us')
- tau = comp i b (eta v @@ j) vs
+ u = theta `face` (i ~> 1)
+ vs = insertsSystem [(j ~> 0, app f theta),(j ~> 1, v)]
+ (Map.map ((@@ j) . sndVal . (@@ i)) us')
+ tau = comp i b (eta v @@ j) vs
+
+-- Every path in the universe induces an equivalence
+eqToEquiv :: Val -> Val
+eqToEquiv e = 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
-------------------------------------------------------------------------------
-- | Conversion
instance Convertible Formula where
conv _ phi psi = dnf phi == dnf psi
+
-------------------------------------------------------------------------------
-- | Normalization
projects / cubicaltt.git / commitdiff