Added Eq types with definitional equality for J

diff --git a/CTT.hs b/CTT.hs
index 944c51c66a3d630aa26bcd5c0db62fa4712cdc41..f974c4b6d6d65822249ffe371a394f4a764405f9 100644 (file)
--- a/CTT.hs
+++ b/CTT.hs
@@ -119,6 +119,10 @@ data Ter = Pi Ter
          | Glue Ter (System Ter)
          | GlueElem Ter (System Ter)
          | UnGlueElem Ter (System Ter)
+           -- Eq
+         | Eq Ter Ter Ter
+         | EqPair Ter (System Ter)
+         | EqJ Ter Ter Ter Ter Ter Ter
   deriving Eq
 
 -- For an expression t, returns (u,ts) where u is no application and t = u ts
@@ -163,6 +167,10 @@ data Val = VU
            -- Composition for HITs; the type is constant
          | VHComp Val Val (System Val)
 
+           -- Eq
+         | VEq Val Val Val
+         | VEqPair Val (System Val)
+
            -- Neutral values:
          | VVar Ident Val
          | VOpaque Ident Val
@@ -173,23 +181,25 @@ data Val = VU
          | VAppFormula Val Formula
          | VLam Ident Val Val
          | VUnGlueElemU Val Val (System Val)
+         | VEqJ Val Val Val Val Val Val
   deriving Eq
 
 isNeutral :: Val -> Bool
 isNeutral v = case v of
-  Ter Undef{} _     -> True
-  Ter Hole{} _      -> True
-  VVar{}            -> True
-  VOpaque{}         -> True
-  VComp{}           -> True
-  VFst{}            -> True
-  VSnd{}            -> True
-  VSplit{}          -> True
-  VApp{}            -> True
-  VAppFormula{}     -> True
-  VUnGlueElemU{}    -> True
-  VUnGlueElem{}     -> True
-  _                 -> False
+  Ter Undef{} _  -> True
+  Ter Hole{} _   -> True
+  VVar{}         -> True
+  VOpaque{}      -> True
+  VComp{}        -> True
+  VFst{}         -> True
+  VSnd{}         -> True
+  VSplit{}       -> True
+  VApp{}         -> True
+  VAppFormula{}  -> True
+  VUnGlueElemU{} -> True
+  VUnGlueElem{}  -> True
+  VEqJ{}         -> True
+  _              -> False
 
 isNeutralSystem :: System Val -> Bool
 isNeutralSystem = any isNeutral . elems
@@ -373,6 +383,9 @@ showTer v = case v of
   Glue a ts          -> text "Glue" <+> showTer1 a <+> text (showSystem ts)
   GlueElem a ts      -> text "glue" <+> showTer1 a <+> text (showSystem ts)
   UnGlueElem a ts    -> text "unglue" <+> showTer1 a <+> text (showSystem ts)
+  Eq a u v           -> text "Eq" <+> showTers [a,u,v]
+  EqPair b ts        -> text "eqC" <+> showTer1 b <+> text (showSystem ts)
+  EqJ a t c d x p    -> text "eqJ" <+> showTers [a,t,c,d,x,p]
 
 showTers :: [Ter] -> Doc
 showTers = hsep . map showTer1

diff --git a/Connections.hs b/Connections.hs
index 077d575df3aec0fd5bedabb6de3470227f8ddcf1..4d8b524946126fc0416993573e9a59419a0d2775 100644 (file)
--- a/Connections.hs
+++ b/Connections.hs
@@ -403,6 +403,11 @@ unionSystem :: System a -> System a -> System a
 unionSystem us vs = insertsSystem (assocs us) vs
 
 
+joinSystem :: System (System a) -> System a
+joinSystem tss = mkSystem $
+  [ (alpha `meet` beta,t) | (alpha,ts) <- assocs tss, (beta,t) <- assocs ts ]
+
+
 -- TODO: add some checks
 transposeSystemAndList :: System [a] -> [b] -> [(System a,b)]
 transposeSystemAndList _  []      = []

diff --git a/Eval.hs b/Eval.hs
index 90d862f2d8cfed40fd0f8ca49318f781e1474360..3b60833c749c360f933f9404afb0af4ccc6568dd 100644 (file)
--- a/Eval.hs
+++ b/Eval.hs
@@ -77,6 +77,9 @@ instance Nominal Val where
     VUnGlueElem a ts        -> support (a,ts)
     VCompU a ts             -> support (a,ts)
     VUnGlueElemU a b es     -> support (a,b,es)
+    VEqPair u us            -> support (u,us)
+    VEq a u v               -> support (a,u,v)
+    VEqJ a u c d x p        -> support [a,u,c,d,x,p]
 
   act u (i, phi) | i `notElem` support u = u
                  | otherwise =
@@ -111,6 +114,10 @@ instance Nominal Val where
          VUnGlueElem a ts        -> unglueElem (acti a) (acti ts)
          VUnGlueElemU a b es     -> unGlueU (acti a) (acti b) (acti es)
          VCompU a ts             -> compUniv (acti a) (acti ts)
+         VEqPair u us            -> VEqPair (acti u) (acti us)
+         VEq a u v               -> VEq (acti a) (acti u) (acti v)
+         VEqJ a u c d x p        ->
+           eqJ (acti a) (acti u) (acti c) (acti d) (acti x) (acti p)
 
   -- This increases efficiency as it won't trigger computation.
   swap u ij@(i,j) =
@@ -141,7 +148,10 @@ instance Nominal Val where
          VUnGlueElem a ts        -> VUnGlueElem (sw a) (sw ts)
          VUnGlueElemU a b es     -> VUnGlueElemU (sw a) (sw b) (sw es)
          VCompU a ts             -> VCompU (sw a) (sw ts)
-
+         VEqPair u us            -> VEqPair (sw u) (sw us)
+         VEq a u v               -> VEq (sw a) (sw u) (sw v)
+         VEqJ a u c d x p        ->
+           VEqJ (sw a) (sw u) (sw c) (sw d) (sw x) (sw p)
 
 -----------------------------------------------------------------------
 -- The evaluator
@@ -179,6 +189,10 @@ eval rho@(_,_,_,Nameless os) v = case v of
   Glue a ts           -> glue (eval rho a) (evalSystem rho ts)
   GlueElem a ts       -> glueElem (eval rho a) (evalSystem rho ts)
   UnGlueElem a ts     -> unglueElem (eval rho a) (evalSystem rho ts)
+  Eq a r s            -> VEq (eval rho a) (eval rho r) (eval rho s)
+  EqPair b ts         -> VEqPair (eval rho b) (evalSystem rho ts)
+  EqJ a t c d x p     -> eqJ (eval rho a) (eval rho t) (eval rho c)
+                             (eval rho d) (eval rho x) (eval rho p)
   _                   -> error $ "Cannot evaluate " ++ show v
 
 evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)]
@@ -266,6 +280,7 @@ inferType v = case v of
   VComp a _ _ -> a @@ One
 --  VUnGlueElem _ b _  -> b   -- This is wrong! Store the type??
   VUnGlueElemU _ b _ -> b
+  VEqJ _ _ c _ x p -> app (app c x) p
   _ -> error $ "inferType: not neutral " ++ show v
 
 (@@) :: ToFormula a => Val -> a -> Val
@@ -292,6 +307,16 @@ comp i a u ts = case a of
   VPathP p v0 v1 -> let j = fresh (Atom i,a,u,ts)
                     in VPLam j $ comp i (p @@ j) (u @@ j) $
                          insertsSystem [(j ~> 0,v0),(j ~> 1,v1)] (Map.map (@@ j) ts)
+  VEq b v0 v1 -> case u of
+    VEqPair r _ | all isEqPair (elems ts) ->
+      let j = fresh (Atom i,a,u,ts)
+          VEqPair z _ @@@ phi = z @@ phi
+          sys (VEqPair _ ws)  = ws
+          w = VPLam j $ comp i b (r @@ j) $
+                          insertsSystem [(j ~> 0,v0),(j ~> 1,v1)]
+                            (Map.map (@@@ j) ts)
+      in VEqPair w (joinSystem (Map.map sys (ts `face` (i ~> 1))))
+    _ -> VComp (VPLam i a) u (Map.map (VPLam i) 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)
@@ -398,6 +423,23 @@ squeezes i xas e us = comps j xas (e `disj` (i,j)) us'
         us' = [ (mkSystem [(i ~> 1, u `face` (i ~> 1))],u) | u <- us ]
 
 
+-------------------------------------------------------------------------------
+-- | Eq
+
+eqJ :: Val -> Val -> Val -> Val -> Val -> Val -> Val
+eqJ a v c d x p = case p of
+  VEqPair w ws -> comp i (app (app c (w @@ i)) w') d
+                    (border d (shape ws))
+    where w' = VEqPair (VPLam j $ w @@ (Atom i :/\: Atom j))
+                  (insertSystem (i ~> 0) v ws)
+          i:j:_ = freshs [a,v,c,d,x,p]
+  _ -> VEqJ a v c d x p
+
+isEqPair :: Val -> Bool
+isEqPair VEqPair{} = True
+isEqPair _         = False
+
+
 -------------------------------------------------------------------------------
 -- | HITs
 
@@ -842,7 +884,11 @@ instance Convertible Val where
       (VUnGlueElemU u _ _,VUnGlueElemU u' _ _) -> conv ns u u'
       (VUnGlueElem u ts,VUnGlueElem u' ts')    -> conv ns (u,ts) (u',ts')
       (VCompU u es,VCompU u' es')              -> conv ns (u,es) (u',es')
-      _                                        -> False
+      (VEqPair v vs,VEqPair v' vs')          -> conv ns (v,vs) (v',vs')
+      (VEq a u v,VEq a' u' v')               -> conv ns (a,u,v) (a',u',v')
+      (VEqJ a u c d x p,VEqJ a' u' c' d' x' p') ->
+        conv ns [a,u,c,d,x,p] [a',u',c',d',x',p']
+      _                                      -> False
 
 instance Convertible Ctxt where
   conv _ _ _ = True
@@ -909,6 +955,10 @@ instance Normal Val where
     VSplit u t          -> VSplit (normal ns u) (normal ns t)
     VApp u v            -> app (normal ns u) (normal ns v)
     VAppFormula u phi   -> VAppFormula (normal ns u) (normal ns phi)
+    VEq a u v           -> VEq (normal ns a) (normal ns u) (normal ns v)
+    VEqPair u us        -> VEqPair (normal ns u) (normal ns us)
+    VEqJ a u c d x p    -> eqJ (normal ns a) (normal ns u) (normal ns c)
+                               (normal ns d) (normal ns x) (normal ns p)
     _                   -> v
 
 instance Normal (Nameless a) where

diff --git a/Exp.cf b/Exp.cf
index d5afd2fa7d99d87f4ebb63f3e71e509dfa976c85..29cfb0e8fc0ece5d4b10aa275e36b953bfae68bd 100644 (file)
--- a/Exp.cf
+++ b/Exp.cf
@@ -42,6 +42,9 @@ Fill.         Exp3 ::= "fill" Exp4 Exp4 System ;
 Glue.         Exp3 ::= "Glue" Exp4 System ;
 GlueElem.     Exp3 ::= "glue" Exp4 System ;
 UnGlueElem.   Exp3 ::= "unglue" Exp4 System ;
+Eq.           Exp3 ::= "Eq" Exp4 Exp4 Exp3 ;
+EqPair.       Exp3 ::= "eqC" Exp4 System ;
+EqJ.          Exp3 ::= "eqJ" Exp4 Exp4 Exp4 Exp4 Exp4 Exp4 ;
 Fst.          Exp4 ::= Exp4 ".1" ;
 Snd.          Exp4 ::= Exp4 ".2" ;
 Pair.         Exp5 ::= "(" Exp "," [Exp] ")" ;

diff --git a/Resolver.hs b/Resolver.hs
index 0871c89e9d4629394886e5addf128ec682487d6a..9cd9890987306c6e5a708a3f92e378a0fe2522c8 100644 (file)
--- a/Resolver.hs
+++ b/Resolver.hs
@@ -219,6 +219,10 @@ resolveExp e = case e of
   Glue u ts     -> CTT.Glue <$> resolveExp u <*> resolveSystem ts
   GlueElem u ts -> CTT.GlueElem <$> resolveExp u <*> resolveSystem ts
   UnGlueElem u ts -> CTT.UnGlueElem <$> resolveExp u <*> resolveSystem ts
+  Eq a u v      -> CTT.Eq <$> resolveExp a <*> resolveExp u <*> resolveExp v
+  EqPair u ts   -> CTT.EqPair <$> resolveExp u <*> resolveSystem ts
+  EqJ a t c d x p -> CTT.EqJ <$> resolveExp a <*> resolveExp t <*> resolveExp c
+                             <*> resolveExp d <*> resolveExp x <*> resolveExp p
   _ -> do
     modName <- asks envModule
     throwError ("Could not resolve " ++ show e ++ " in module " ++ modName)

diff --git a/TypeChecker.hs b/TypeChecker.hs
index 2427e0221754e380f28de3c60429489ad4326c9f..8b74327d24a671e3bb3297adc52ca65f5ee88242 100644 (file)
--- a/TypeChecker.hs
+++ b/TypeChecker.hs
@@ -215,6 +215,22 @@ check a t = case (a,t) of
     check va u\r
     vu <- evalTyping u\r
     checkGlueElemU vu ves us\r
+  (VU,Eq a a0 a1) -> do\r
+    check VU a\r
+    va <- evalTyping a\r
+    check va a0\r
+    check va a1\r
+  (VEq va va0 va1,EqPair w ts) -> do\r
+    check (VPathP (constPath va) va0 va1) w\r
+    vw <- evalTyping w\r
+    checkSystemWith ts $ \alpha tAlpha ->\r
+      local (faceEnv alpha) $ do\r
+        check (va `face` alpha) tAlpha\r
+        vtAlpha <- evalTyping tAlpha\r
+        unlessM (vw `face` alpha === constPath vtAlpha) $\r
+          throwError "malformed eqC"\r
+    rho <- asks env\r
+    checkCompSystem (evalSystem rho ts) -- Not needed\r
   _ -> do\r
     v <- infer t\r
     unlessM (v === a) $\r
@@ -338,6 +354,8 @@ mkEquiv va = eval rho $
 checkEquiv :: Val -> Ter -> Typing ()\r
 checkEquiv va equiv = check (mkEquiv va) equiv\r
 \r
+checkIso :: Val -> Ter -> Typing ()\r
+checkIso vb iso = check (mkIso vb) iso\r
 \r
 checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()\r
 checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do\r
@@ -480,6 +498,23 @@ infer e = case e of
     checks (bs,nu) es\r
     mapM_ checkFormula phis\r
     return va\r
+  EqJ a u c d x p -> do\r
+    check VU a\r
+    va <- evalTyping a\r
+    check va u\r
+    vu <- evalTyping u\r
+    let refu = VEqPair (constPath vu) $ mkSystem [(eps,vu)]\r
+    rho <- asks env\r
+    let z = Var "z"\r
+        ctype = eval rho $ Pi $ Lam "z" a $ Pi $ Lam "_" (Eq a u z) U\r
+    check ctype c\r
+    vc <- evalTyping c\r
+    check (app (app vc vu) refu) d\r
+    check va x\r
+    vx <- evalTyping x\r
+    check (VEq va vu vx) p\r
+    vp <- evalTyping p\r
+    return (app (app vc vx) vp)\r
   _ -> throwError ("infer " ++ show e)\r
 \r
 -- Not used since we have U : U\r