From: Simon Huber <hubsim@gmail.com>
Date: Thu, 4 Jun 2015 09:06:40 +0000 (+0200)
Subject: Fix for neutral unglues
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=bdcb90f823a9025a4b9cb7194ed7bd9d4abab01a;p=cubicaltt.git

Fix for neutral unglues
---

diff --git a/CTT.hs b/CTT.hs
index a0e08ee..01f727b 100644
--- a/CTT.hs
+++ b/CTT.hs
@@ -94,7 +94,8 @@ data Ter = App Ter Ter
            -- branches c1 xs1  -> M1,..., cn xsn -> Mn
          | Split Ident Loc Ter [Branch]
            -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors)
-         | Sum Loc Ident [Label]
+         | Sum Loc Ident [Label] -- TODO: should only contain OLabels
+         | HSum Loc Ident [Label]
 
            -- undefined and holes
          | Undef Loc Ter -- Location and type
@@ -157,6 +158,9 @@ data Val = VU
            -- Composition in the universe (for now)
          | VCompU Val (System Val)
 
+           -- Composition for HITs; the type is constant
+         | VHComp Val Val (System Val)
+
            -- GlueLine values
          -- | VGlueLine Val Formula Formula
          -- | VGlueLineElem Val Formula Formula
@@ -169,9 +173,11 @@ data Val = VU
          | VVar Ident Val
          | VFst Val
          | VSnd Val
-         | VUnGlueElem Val (System Val)
-         | VUnGlueElemU Val (System Val)
+           -- VUnGlueElem val type hisos
+         | VUnGlueElem Val Val (System Val)
+         | VUnGlueElemU Val Val (System Val)
          | VSplit Val Val
+         | VSqueezeH Val Val
          | VApp Val Val
          | VAppFormula Val Formula
          | VLam Ident Val Val
@@ -395,6 +401,7 @@ showTer v = case v of
                         <+> hsep (map ((char '@' <+>) . showFormula) phis)
   Split f _ _ _      -> text f
   Sum _ n _          -> text n
+  HSum _ n _         -> text n
   Undef{}            -> text "undefined"
   Hole{}             -> text "?"
   IdP e0 e1 e2       -> text "IdP" <+> showTers [e0,e1,e2]
@@ -426,6 +433,7 @@ showTer1 t = case t of
   Hole{}   -> showTer t
   Split{}  -> showTer t
   Sum{}    -> showTer t
+  HSum{}   -> showTer t
   _        -> parens (showTer t)
 
 showDecls :: [Decl] -> Doc
@@ -439,11 +447,13 @@ showVal :: Val -> Doc
 showVal v = case v of
   VU                -> char 'U'
   Ter t@Sum{} rho   -> showTer t <+> showEnv False rho
+  Ter t@HSum{} rho  -> showTer t <+> showEnv False rho
   Ter t@Split{} rho -> showTer t <+> showEnv False rho
   Ter t rho         -> showTer1 t <+> showEnv True rho
   VCon c us         -> text c <+> showVals us
   VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us
                        <+> hsep (map ((char '@' <+>) . showFormula) phis)
+  VHComp v0 v1 vs   -> text "hComp" <+> showVals [v0,v1] <+> text (showSystem vs)
   VPi a l@(VLam x t b)
     | "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b
     | otherwise          -> char '(' <> showLam v
@@ -457,8 +467,10 @@ showVal v = case v of
   VVar x _          -> text x
   VFst u            -> showVal1 u <> text ".1"
   VSnd u            -> showVal1 u <> text ".2"
-  VUnGlueElem v hs  -> text "unGlueElem" <+> showVal1 v <+> text (showSystem hs)
-  VUnGlueElemU v es -> text "unGlueElemU" <+> showVal1 v <+> text (showSystem es)
+  VUnGlueElem v b hs  -> text "unGlueElem" <+> showVals [v,b]
+                         <+> text (showSystem hs)
+  VUnGlueElemU v b es -> text "unGlueElemU" <+> showVals [v,b]
+                         <+> text (showSystem es)
   VIdP v0 v1 v2     -> text "IdP" <+> showVals [v0,v1,v2]
   VAppFormula v phi -> showVal v <+> char '@' <+> showFormula phi
   VComp v0 v1 vs    -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
diff --git a/Eval.hs b/Eval.hs
index 713e9aa..5e847c7 100644
--- a/Eval.hs
+++ b/Eval.hs
@@ -68,6 +68,7 @@ instance Nominal Val where
     VSnd u                  -> support u
     VCon _ vs               -> support vs
     VPCon _ a vs phis       -> support (a,vs,phis)
+    VHComp a u ts           -> support (a,u,ts)
     VVar _ v                -> support v
     VApp u v                -> support (u,v)
     VLam _ u v              -> support (u,v)
@@ -76,8 +77,8 @@ instance Nominal Val where
     VGlue a ts              -> support (a,ts)
     VGlueElem a ts          -> support (a,ts)
     VCompU a ts             -> support (a,ts)
-    VUnGlueElem a hs        -> support (a,hs)
-    VUnGlueElemU a es       -> support (a,es)
+    VUnGlueElem a b hs      -> support (a,b,hs)
+    VUnGlueElemU a b es     -> support (a,b,es)
     -- VGlueLine a phi psi     -> support (a,phi,psi)
     -- VGlueLineElem a phi psi -> support (a,phi,psi)
     -- VCompElem a es u us     -> support (a,es,u,us)
@@ -105,6 +106,7 @@ instance Nominal Val where
          VSnd u                  -> sndVal (acti u)
          VCon c vs               -> VCon c (acti vs)
          VPCon c a vs phis       -> pcon c (acti a) (acti vs) (acti phis)
+         VHComp a u us           -> VHComp (acti a) (acti u) (acti us)
          VVar x v                -> VVar x (acti v)
          VAppFormula u psi       -> acti u @@ acti psi
          VApp u v                -> app (acti u) (acti v)
@@ -112,8 +114,8 @@ instance Nominal Val where
          VSplit u v              -> app (acti u) (acti v)
          VGlue a ts              -> glue (acti a) (acti ts)
          VGlueElem a ts          -> glueElem (acti a) (acti ts)
-         VUnGlueElem a hs        -> unGlue (acti a) (acti hs)
-         VUnGlueElemU a es       -> unGlueU (acti a) (acti es)
+         VUnGlueElem a b hs      -> unGlue (acti a) (acti b) (acti hs)
+         VUnGlueElemU a b es     -> unGlueU (acti a) (acti b) (acti es)
          VCompU a ts             -> compUniv (acti a) (acti ts)
          -- VGlueLine a phi psi     -> glueLine (acti a) (acti phi) (acti psi)
          -- VGlueLineElem a phi psi -> glueLineElem (acti a) (acti phi) (acti psi)
@@ -138,6 +140,7 @@ instance Nominal Val where
          VSnd u                  -> VSnd (sw u)
          VCon c vs               -> VCon c (sw vs)
          VPCon c a vs phis       -> VPCon c (sw a) (sw vs) (sw phis)
+         VHComp a u us           -> VHComp (sw a) (sw u) (sw us)
          VVar x v                -> VVar x (sw v)
          VAppFormula u psi       -> VAppFormula (sw u) (sw psi)
          VApp u v                -> VApp (sw u) (sw v)
@@ -145,8 +148,8 @@ instance Nominal Val where
          VSplit u v              -> VSplit (sw u) (sw v)
          VGlue a ts              -> VGlue (sw a) (sw ts)
          VGlueElem a ts          -> VGlueElem (sw a) (sw ts)
-         VUnGlueElem a hs        -> VUnGlueElem (sw a) (sw hs)
-         VUnGlueElemU a es       -> VUnGlueElemU (sw a) (sw es)
+         VUnGlueElem a b hs      -> VUnGlueElem (sw a) (sw b) (sw hs)
+         VUnGlueElemU a b es     -> VUnGlueElemU (sw a) (sw b) (sw es)
          VCompU a ts             -> VCompU (sw a) (sw ts)
          -- VGlueLine a phi psi     -> VGlueLine (sw a) (sw phi) (sw psi)
          -- VGlueLineElem a phi psi -> VGlueLineElem (sw a) (sw phi) (sw psi)
@@ -173,6 +176,7 @@ eval rho v = case v of
   Lam{}               -> Ter v rho
   Split{}             -> Ter v rho
   Sum{}               -> Ter v rho
+  HSum{}              -> Ter v rho
   Undef{}             -> Ter v rho
   Hole{}              -> Ter v rho
   IdP a e0 e1         -> VIdP (eval rho a) (eval rho e0) (eval rho e1)
@@ -289,6 +293,8 @@ inferType v = case v of
     ty         -> error $ "inferType: expected IdP type for " ++ show v
                   ++ ", got " ++ show ty
   VComp a _ _ -> a @@ One
+  VUnGlueElem _ b hs  -> glue b hs
+  VUnGlueElemU _ b es -> compUniv b es
 --  VTrans a _  -> a @@ One
   _ -> error $ "inferType: not neutral " ++ show v
 
@@ -304,7 +310,7 @@ v @@ phi | isNeutral v     = case (inferType v,toFormula phi) of
 v @@ phi                   = error $ "(@@): " ++ show v ++ " should be neutral."
 
 pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val
-pcon c a@(Ter (Sum _ _ lbls) rho) us phis = case lookupPLabel c lbls of
+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)
@@ -453,11 +459,8 @@ comp i a u ts = case a of
                 in VCon n $ comps i as env tsus
            else VComp (VPath i a) u (Map.map (VPath i) ts)
       Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
-    VPCon{} -> compHIT i a u ts
-    VComp{} -> VComp (VPath i a) u (Map.map (VPath i) ts)
-    -- VCompElem _ _ u1 _  -> comp i a u1 ts
-    -- VElimComp _ _ u1    -> comp i a u1 ts
     _ -> error $ "comp ter sum" ++ show u
+  Ter (HSum _ _ nass) env -> compHIT i a u ts
   _ -> VComp (VPath i a) u (Map.map (VPath i) ts)
   -- _ -> error $ "comp: case missing for " ++ show i ++ " " ++ show a ++ " " ++ show u ++ " " ++ showSystem ts
 
@@ -478,9 +481,25 @@ compNeg i a u ts = comp i (a `sym` i) u (ts `sym` i)
 compHIT :: Name -> Val -> Val -> System Val -> Val
 compHIT = undefined
 
+
+-- case u of
+--     VCon n us -> case lookupLabel n nass of
+--       Just as ->
+--         if all isCon (elems ts)
+--            then let tsus = transposeSystemAndList (Map.map unCon ts) us
+--                 in VCon n $ comps i as env tsus
+--            else VComp (VPath i a) u (Map.map (VPath i) ts)
+--       Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
+--     VPCon{} -> compHIT i a u ts
+--     VComp{} -> VComp (VPath i a) u (Map.map (VPath i) ts)
+--     _ -> error $ "comp ter sum" ++ show u
+
+
 transpHIT :: Name -> Val -> Val -> Val
-transpHIT = undefined
+transpHIT i a u = squeezeHIT i a u `face` (i ~> 0)
 
+-- Given u(i) of type a(i) "squeezeHIT i a u" connects in the direction i
+-- transHIT i a u(i=0) to u(i=1) in a(1)
 squeezeHIT :: Name -> Val -> Val -> Val
 squeezeHIT = undefined
 
@@ -517,15 +536,15 @@ glueElem v us | Map.null us         = v
               | eps `Map.member` us = us ! eps
               | otherwise           = VGlueElem v us
 
-unGlue :: Val -> System Val -> Val
-unGlue w hisos
+unGlue :: Val -> Val -> System Val -> Val
+unGlue w b hisos
     | Map.null hisos         = w
     | eps `Map.member` hisos = app (hisoFun (hisos ! eps)) w
     | otherwise              = case w of
        VGlueElem v us   -> v
        -- VElimComp _ _ v -> unGlue hisos v
        -- VCompElem a es v vs -> unGlue hisos v
-       _ -> VUnGlueElem w hisos
+       _ -> VUnGlueElem w b hisos
 
 -- transGlue :: Name -> Val -> System Val -> Val -> Val
 -- transGlue i b hisos wi0 = glueElem vi1'' usi1
@@ -571,9 +590,10 @@ compGlue :: Name -> Val -> System Val -> Val -> System Val -> Val
 compGlue i b hisos wi0 ws = glueElem vi1'' usi1''
   where bi1 = b `face` (i ~> 1)
         vs   = mapWithKey
-                 (\alpha wAlpha -> unGlue wAlpha (hisos `face` alpha)) ws
+                 (\alpha wAlpha -> unGlue wAlpha
+                                     (b `face` alpha) (hisos `face` alpha)) ws
         vsi1 = vs `face` (i ~> 1) -- same as: border vi1 vs
-        vi0  = unGlue wi0 (hisos `face` (i ~> 0)) -- in b(i0)
+        vi0  = unGlue wi0 (b `face` (i ~> 0)) (hisos `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)
@@ -770,13 +790,13 @@ gradLemma b hiso@(VPair a (VPair f (VPair g (VPair s t)))) us v =
 -------------------------------------------------------------------------------
 -- | Composition in the Universe (to be replaced as glue)
 
-unGlueU :: Val -> System Val -> Val
-unGlueU w es
+unGlueU :: Val -> Val -> System Val -> Val
+unGlueU w b es
     | Map.null es         = w
     | eps `Map.member` es = transNegLine (es ! eps) w
     | otherwise           = case w of
        VGlueElem v us   -> v
-       _ -> VUnGlueElemU w es
+       _ -> VUnGlueElemU w b es
 
 compUniv :: Val -> System Val -> Val
 compUniv b es | Map.null es         = b
@@ -787,9 +807,10 @@ compUniv b es | Map.null es         = b
 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 (es `face` alpha)) ws
+        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 (es `face` (i ~> 0)) -- in b(i0)
+        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)
@@ -1065,8 +1086,8 @@ instance Convertible Val where
       (VComp a u ts,VComp a' u' ts') -> conv ns (a,u,ts) (a',u',ts')
       (VGlue v hisos,VGlue v' hisos') -> conv ns (v,hisos) (v',hisos')
       (VGlueElem u us,VGlueElem u' us') -> conv ns (u,us) (u',us')
-      (VUnGlueElem _ u,VUnGlueElem _ u') -> conv ns u u'
-      (VUnGlueElemU _ u,VUnGlueElemU _ u') -> conv ns u u'
+      (VUnGlueElem u _ _,VUnGlueElem u' _ _) -> conv ns u u'
+      (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'
       -- (VCompElem a es u us,VCompElem a' es' u' us') ->
       --   conv ns (a,es,u,us) (a',es',u',us')
       -- (VElimComp a es u,VElimComp a' es' u') -> conv ns (a,es,u) (a',es',u')
@@ -1125,8 +1146,8 @@ instance Normal Val where
     -- VTrans u v          -> transLine (normal ns u) (normal ns v)
     VGlue u hisos       -> glue (normal ns u) (normal ns hisos)
     VGlueElem u us      -> glueElem (normal ns u) (normal ns us)
-    VUnGlueElem u hs    -> unGlue (normal ns u) (normal ns hs)
-    VUnGlueElemU u es   -> unGlueU (normal ns u) (normal ns es)
+    VUnGlueElem u b hs  -> unGlue (normal ns u) (normal ns b) (normal ns hs)
+    VUnGlueElemU u b es -> unGlueU (normal ns u) (normal ns b) (normal ns es)
     VCompU u es         -> compUniv (normal ns u) (normal ns es)
     -- VCompElem a es u us -> compElem (normal ns a) (normal ns es) (normal ns u) (normal ns us)
     -- VElimComp a es u    -> elimComp (normal ns a) (normal ns es) (normal ns u)