Added fill as a term and comp is now genComp

diff --git a/CTT.hs b/CTT.hs
index 1e9f5dedcf39a4394c597bf618575920a60444cb..3dbe30cd86d2832addf9339631653164b2edbac9 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -105,8 +105,9 @@ data Ter = App Ter Ter
          | IdP Ter Ter Ter
          | Path Name Ter
          | AppFormula Ter Formula
-           -- Kan Composition
+           -- Kan composition and filling
          | Comp Ter Ter (System Ter)
+         | Fill Ter Ter (System Ter)
          -- | Trans Ter Ter
            -- Composition in the Universe
          -- | CompElem Ter (System Ter) Ter (System Ter)
@@ -183,15 +184,6 @@ data Val = VU
          | VLam Ident Val Val
   deriving Eq
 
--- data HIso = Iso Val Val Val Val Val
---           | Eq Val
---   deriving (Eq,Show)
-
--- toHIso :: Val -> HIso
--- toHIso (VPair a (VPair f (VPair g (VPair s t)))) = Iso a f g s t
--- toHIso v = Eq v
--- toHIso _ = error "toHIso"
-
 isNeutral :: Val -> Bool
 isNeutral v = case v of
   Ter Undef{} _  -> True
@@ -407,8 +399,8 @@ showTer v = case v of
   IdP e0 e1 e2       -> text "IdP" <+> showTers [e0,e1,e2]
   Path i e           -> char '<' <> text (show i) <> char '>' <+> showTer e
   AppFormula e phi   -> showTer1 e <+> char '@' <+> showFormula phi
-  Comp e0 e1 es      -> text "comp" <+> showTers [e0,e1]
-                        <+> text (showSystem es)
+  Comp e t ts        -> text "comp" <+> showTers [e,t] <+> text (showSystem ts)
+  Fill e t ts        -> text "fill" <+> showTers [e,t] <+> text (showSystem ts)
   -- Trans e0 e1        -> text "transport" <+> showTers [e0,e1]
   Glue a ts          -> text "glue" <+> showTer1 a <+> text (showSystem ts)
   GlueElem a ts      -> text "glueElem" <+> showTer1 a <+> text (showSystem ts)

diff --git a/Eval.hs b/Eval.hs
index 3144eefdd010cfe1271f97c1143c5db33ae378e4..db7827e84715d84465192d8411cfa1401e61e390 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -159,6 +159,7 @@ eval rho v = case v of
     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)
   Glue a ts           -> glue (eval rho a) (evalSystem rho ts)
   GlueElem a ts       -> glueElem (eval rho a) (evalSystem rho ts)
   _                   -> error $ "Cannot evaluate " ++ show v
@@ -443,6 +444,25 @@ hisoFun :: Val -> Val
 hisoFun (VPair _ (VPair f _)) = f
 hisoFun x                     = error $ "HisoFun: Not an hiso: " ++ show x
 
+-- -- Every line in the universe induces an hiso
+-- eqToIso :: Val -> Val
+-- eqToIso e = VPair e0 (VPair f (VPair g (VPair s t)))
+--   where e0 = e @@ Zero
+--         (i,j,x,y,ev) = (Name "i",Name "j",Var "x",Var "y",Var "E")
+--         evinv = Path "i" $ AppFormula ev (NegAtom i)
+--         (ev0, ev1) = (AppFormula ev (Dir Zero),AppFormula ev (Dir One))
+--         eenv = upd ("E",e) empty
+--         (eplus z,eminus z) = (Comp ev z Map.empty,Comp evinv z Map.empty)
+--         (eup z,edown z) = (Comp )
+--         f = Ter (Lam x ev1 (eminus x)) eenv
+--         g = Ter (Lam y ev0 (eplus y)) eenv
+--         -- s : (y : b) -> f (g y) = y
+--         ssys = mkSystem [(j ~> 0, transFill j (e @@ j) b)
+--                         ,(j ~> 1, transFillNeg j (e @@ j)
+--                                   (trans j (e @@ j) b))])
+--         s = Ter (Lam y ev0 $ Path j $ Comp einv
+--               ) eenv
+
 -- eqToIso :: Name -> Val -> Val
 -- eqToIso i u = VPair a (VPair f (VPair g (VPair s t)))
 --   where a = u `face` (i ~> 1)

diff --git a/Exp.cf b/Exp.cf
index 0c0dcf3ef9cf6f1e622000d89d054afab4d5b181..718647da36c408c81d88061091f4884f74fa4d8a 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -33,7 +33,7 @@ App.          Exp2 ::= Exp2 Exp3 ;
 IdP.          Exp3 ::= "IdP" Exp4 Exp4 Exp4 ;
 Trans.        Exp3 ::= "transport" Exp4 Exp4 ;
 Comp.         Exp3 ::= "comp" Exp4 Exp4 System ;
-GenComp.      Exp3 ::= "genComp" Exp4 Exp4 System ;
+Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "glue" Exp4 System ;
 -- GlueElem.     Exp3 ::= "glueElem" Exp4 System ;
 -- CompElem.     Exp3 ::= "compElem" Exp4 System Exp4 System ;

diff --git a/Resolver.hs b/Resolver.hs
index 60c9ebc7c41ca75e9f3986d19e5f3352f16d1f0c..734d5c945a1825b46a7512be0b85b095d154cf65 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -204,11 +204,8 @@ resolveExp e = case e of
       _ -> CTT.AppFormula <$> resolveExp t <*> resolveFormula phi
   Trans x y   -> CTT.Comp <$> resolveExp x <*> resolveExp y <*> pure Map.empty
   IdP x y z   -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
-  Comp u v ts -> CTT.Comp <$> (CTT.Path (C.Name "_") <$> resolveExp u)
-                   <*> resolveExp v <*> resolveSystem ts
-
-  GenComp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
-
+  Comp u v ts -> CTT.Comp <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
+  Fill u v ts -> CTT.Fill <$> resolveExp u <*> resolveExp v <*> resolveSystem ts
   Glue u ts   -> do
     rs <- resolveSystem ts
     let isIso (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ (CTT.Pair _ _)))) = True

diff --git a/TypeChecker.hs b/TypeChecker.hs
index c94f8abed1733789c6c72f917b1fa4a2102687f5..82f51bf331472626d1b5daa82ea0971214d8f843 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -429,6 +429,15 @@ infer e = case e of
     check va0 t0\r
     checkPathSystem t0 va ps\r
     return va1\r
+  Fill a t0 ps -> do\r
+    (va0, va1) <- checkPath (constPath VU) a\r
+    va <- evalTyping a\r
+    check va0 t0\r
+    checkPathSystem t0 va ps\r
+    vt  <- evalTyping t0\r
+    rho <- asks env\r
+    let vps = evalSystem rho ps\r
+    return (VIdP va vt (compLine va vt vps))\r
   -- CompElem a es u us -> do\r
   --   check VU a\r
   --   rho <- asks env\r