From 33ebab86a5f6aaf07bfab3fb39f7ae829ebbf2b0 Mon Sep 17 00:00:00 2001 From: Simon Huber Date: Tue, 9 Jun 2015 15:48:42 +0200 Subject: [PATCH] Rename hiso to equiv --- CTT.hs | 2 +- Eval.hs | 71 +++++++++++++++++++++++--------------------------- TypeChecker.hs | 27 ++++--------------- 3 files changed, 38 insertions(+), 62 deletions(-) diff --git a/CTT.hs b/CTT.hs index 1b8a687..edd290b 100644 --- a/CTT.hs +++ b/CTT.hs @@ -163,7 +163,7 @@ data Val = VU | VVar Ident Val | VFst Val | VSnd Val - -- VUnGlueElem val type hisos + -- VUnGlueElem val type equivs | VUnGlueElem Val Val (System Val) | VSplit Val Val | VApp Val Val diff --git a/Eval.hs b/Eval.hs index 2c02e03..67fe378 100644 --- a/Eval.hs +++ b/Eval.hs @@ -359,7 +359,7 @@ comp i a u ts = case a of 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 hisos -> compGlue i b hisos u 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 @@ -421,15 +421,6 @@ hComp a u us | eps `Map.member` us = (us ! eps) @@ One ------------------------------------------------------------------------------- -- | Glue --- --- OLD: --- An hiso 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 - -- An equivalence for a type b is a four-tuple (a,f,s,t) where -- a : U -- f : a -> b @@ -437,15 +428,17 @@ hComp a u us | eps `Map.member` us = (us ! eps) @@ One -- t : (y : b) (w : fiber a b f y) -> s y = w -- with fiber a b f y = (x : a) * (f x = y) -hisoDom :: Val -> Val -hisoDom (VPair a _) = a -hisoDom x = error $ "HisoDom: Not an hiso: " ++ show x +equivDom :: Val -> Val +equivDom (VPair a _) = a +equivDom x = error $ "equivDom: Not an equivalence: " ++ show x -hisoFun :: Val -> Val -hisoFun (VPair _ (VPair f _)) = f -hisoFun x = error $ "HisoFun: Not an hiso: " ++ show x +equivFun :: Val -> Val +equivFun (VPair _ (VPair f _)) = f +equivFun x = + error $ "equivFun: Not an equivalence: " ++ show x --- -- Every path in the universe induces an hiso +-- 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))) where e1 = e @@ One @@ -473,7 +466,7 @@ eqToIso e = VPair e1 (VPair f (VPair g (VPair s t))) t = Ter (Lam "x" ev1 $ Path j $ Comp ev (eminus x) tsys) eenv glue :: Val -> System Val -> Val -glue b ts | eps `Map.member` ts = hisoDom (ts ! eps) +glue b ts | eps `Map.member` ts = equivDom (ts ! eps) | otherwise = VGlue b ts glueElem :: Val -> System Val -> Val @@ -481,54 +474,54 @@ glueElem v us | eps `Map.member` us = us ! eps | otherwise = VGlueElem v us unGlue :: Val -> Val -> System Val -> Val -unGlue w b hisos - | eps `Map.member` hisos = app (hisoFun (hisos ! eps)) w +unGlue w b equivs + | eps `Map.member` equivs = app (equivFun (equivs ! eps)) w | otherwise = case w of VGlueElem v us -> v - _ -> VUnGlueElem w b hisos + _ -> VUnGlueElem w b equivs compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val -compGlue i b hisos wi0 ws = glueElem vi1'' usi1'' +compGlue i b equivs wi0 ws = glueElem vi1'' usi1'' where bi1 = b `face` (i ~> 1) vs = mapWithKey (\alpha wAlpha -> unGlue wAlpha - (b `face` alpha) (hisos `face` alpha)) ws + (b `face` alpha) (equivs `face` alpha)) ws vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs - vi0 = unGlue wi0 (b `face` (i ~> 0)) (hisos `face` (i ~> 0)) -- in b(i0) + vi0 = unGlue wi0 (b `face` (i ~> 0)) (equivs `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) - hisosI1 = hisos `face` (i ~> 1) - hisos' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) hisos - hisos'' = filterWithKey (\alpha _ -> alpha `Map.notMember` hisos') hisosI1 + equivsI1 = equivs `face` (i ~> 1) + equivs' = filterWithKey (\alpha _ -> i `Map.notMember` alpha) equivs + equivs'' = filterWithKey (\alpha _ -> alpha `Map.notMember` equivs') equivsI1 us' = mapWithKey (\gamma isoG -> - fill i (hisoDom isoG) (wi0 `face` gamma) (ws `face` gamma)) - hisos' + fill i (equivDom isoG) (wi0 `face` gamma) (ws `face` gamma)) + equivs' usi1' = mapWithKey (\gamma isoG -> - comp i (hisoDom isoG) (wi0 `face` gamma) (ws `face` gamma)) - hisos' + comp i (equivDom isoG) (wi0 `face` gamma) (ws `face` gamma)) + equivs' ls' = mapWithKey (\gamma isoG -> pathComp i (b `face` gamma) (v `face` gamma) - (hisoFun isoG `app` (us' ! gamma)) (vs `face` gamma)) - hisos' + (equivFun isoG `app` (us' ! gamma)) (vs `face` gamma)) + equivs' vi1' = compLine (constPath bi1) vi1 (ls' `unionSystem` Map.map constPath vsi1) wsi1 = ws `face` (i ~> 1) - -- for gamma in hisos'', (i1) gamma is in hisos, so wsi1 gamma + -- for gamma in equivs'', (i1) gamma is in equivs, 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)) - hisos'' + equivs'' - vsi1' = Map.map constPath $ border vi1' hisos' `unionSystem` vsi1 + vsi1' = Map.map constPath $ border vi1' equivs' `unionSystem` vsi1 vi1'' = compLine (constPath bi1) vi1' (Map.map snd uls'' `unionSystem` vsi1') @@ -536,7 +529,7 @@ compGlue i b hisos wi0 ws = glueElem vi1'' usi1'' usi1'' = Map.mapWithKey (\gamma _ -> if gamma `Map.member` usi1' then usi1' ! gamma else fst (uls'' ! gamma)) - hisosI1 + equivsI1 -- assumes u and u' : A are solutions of us + (i0 -> u(i0)) @@ -647,7 +640,7 @@ instance Convertible Val where (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 hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos') + (VGlue v equivs,VGlue v' equivs') -> conv ns (v,equivs) (v',equivs') (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us') (VUnGlueElem u _ _,VUnGlueElem u' _ _) -> conv ns u u' _ -> False @@ -702,7 +695,7 @@ instance Normal Val where VIdP a u0 u1 -> VIdP (normal ns a) (normal ns u0) (normal ns u1) VPath i u -> VPath i (normal ns u) VComp u v vs -> compLine (normal ns u) (normal ns v) (normal ns vs) - VGlue u hisos -> glue (normal ns u) (normal ns hisos) + VGlue u equivs -> glue (normal ns u) (normal ns equivs) VGlueElem u us -> glueElem (normal ns u) (normal ns us) VUnGlueElem u b hs -> unGlue (normal ns u) (normal ns b) (normal ns hs) VVar x t -> VVar x t -- (normal ns t) diff --git a/TypeChecker.hs b/TypeChecker.hs index 857f04b..13d0ba7 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -299,45 +299,28 @@ checkGlueElem vu ts us = do unless (keys ts == keys us) (throwError ("Keys don't match in " ++ show ts ++ " and " ++ show us)) rho <- asks env - checkSystemsWith ts us (\_ vt u -> check (hisoDom vt) u) + checkSystemsWith ts us (\_ vt u -> check (equivDom vt) u) let vus = evalSystem rho us checkSystemsWith ts vus (\alpha vt vAlpha -> - unlessM (app (hisoFun 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) --- -- 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 --- checkIso :: Val -> Ter -> Typing () --- checkIso vb (Pair a (Pair f (Pair g (Pair s t)))) = do --- check VU a --- va <- evalTyping a --- check (mkFun va vb) f --- check (mkFun vb va) g --- vf <- evalTyping f --- vg <- evalTyping g --- check (mkSection vb vf vg) s --- check (mkSection va vg vf) t - -- 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) -checkIso :: Val -> Ter -> Typing () -checkIso vb (Pair a (Pair f (Pair s t))) = do +checkEquiv :: Val -> Ter -> Typing () +checkEquiv vb (Pair a (Pair f (Pair s t))) = do check VU a va <- evalTyping a check (mkFun va vb) f -- 2.34.1