implement glueing and composition for glue

examples/axiom_j.itt

@@ -0,0 +1,23 @@
+let
+  sym : (A : Type) (x y : A) -> Path (\x -> A) x y -> Path (\x -> A) y x
+    = λ A x y p i -> p (~ i)
+in let
+  funext : (A : Type) (B : A -> Type) (f g : (x : A) -> B x) -> ((x : A) -> Path (\i -> B x) (f x) (g x)) -> Path (\i -> (x : A) -> B x) f g
+    = λ A B f g h i x -> h x i
+in let
+  i0IsI1 : Path (\x -> I) i0 i1
+    = λ i -> i
+in let
+  singContr : (A : Type) (a b : A) (p : Path (\j -> A) a b) -> Path (\i -> (x : A) * (Path (\j -> A) a x)) (a, \i -> a) (b, p)
+    = λ A a b p i -> (p i, λ j -> p (i && j))
+in let
+  transport : (A : I -> Type) (a : A i0) -> A i1
+    = \A a -> comp A i0 (\i -> []) a
+in let
+  Jay : (A : Type) (x : A)
+        (P : (y : A) -> Path (\i -> A) x y -> Type)
+        (d : P x (\i -> x))
+        (y : A) (p : Path (\i -> A) x y)
+     -> P y p
+    = \A x P d y p -> transport (\i -> P (p i) (\j -> p (i && j))) d
+in Jay

examples/univalence.itt

@@ -0,0 +1,74 @@
+let Id : (A : Type) -> A -> A -> Type = \A x y -> Path (\i -> A) x y in
+let the : (A : Type) -> A -> A = \A x -> x in
+let
+  fill : (i : I) (A : I -> Type)
+         (phi : I) (u : (i : I) -> Partial phi (A i))
+      -> Sub (A i0) phi (u i0) -> A i
+    = \i A phi u a0 ->
+      comp (\j -> A (i && j)) (phi || ~i) (\j -> [ phi -> u (i && j), ~i -> a0 ]) a0
+in let
+  trans : (A : Type) (a b c : A)
+       -> Path (\i -> A) a b
+       -> Path (\i -> A) b c
+       -> Path (\i -> A) a c
+    = \A a b c p q i ->
+      comp (\j -> A) (i || ~i)
+           (\j -> [ ~i -> a, i -> q j ])
+           (p i)
+in
+let isContr : Type -> Type
+      = \A -> (x : A) * (y : A) -> Path (\i -> A) x y in
+let fiber : (T A : Type) -> (T -> A) -> A -> Type
+      = \T A f y -> (x : T) * Path (\i -> A) y (f x) in
+let isEquiv : (T A : Type) -> (T -> A) -> Type
+      = \T A f -> (y : A) -> isContr (fiber T A f y) in
+let idFun : (B : Type) -> B -> B = \A x -> x in
+let idEquiv : (B : Type) -> isEquiv B B (idFun B)
+    = \B y -> ((y, \i -> y), \u -> \i -> (u.2 i, \j -> u.2 (i && j))) in
+let equiv : (A B : Type) -> Type
+      = \A B -> (f : A -> B) * isEquiv A B f in
+let
+  univalence : (A B : Type) -> equiv A B -> Path (\i -> Type) A B
+    = \A B fun i -> Glue B (i || ~i) [~i -> A, i -> B] [~i -> fun, i -> (idFun B, idEquiv B)]
+in
+let idToEquiv : (A B : Type) -> Path (\i -> Type) A B -> equiv A B
+      = \A B p -> comp (\i -> equiv A (p i)) i0 (\i -> []) (idFun A,
+      idEquiv A)
+in
+let transp : (A B : Type) (p : Path (\i -> Type) A B) -> A -> B = \A B p -> comp (\i -> p i) i0 (\j -> []) in
+let
+  univalenceBeta : (A B : Type) (f : equiv A B)
+    -> Id (A -> B) (transp A B (univalence A B f)) f.1
+    = \A B f i a ->
+      let b : B = transp B B (\i -> B) (f.1 a) in
+      let rem1 : Id B b (f.1 a) = \i -> fill ~i (\i -> B) i0 (\j -> []) (f.1 a) in
+      let rem2 : Id B (transp B B (\i -> B) b) b = \i -> fill ~i (\i -> B) i0 (\j -> []) b in
+      let goal : Id B (transp B B (\i -> B) b) (f.1 a) = 
+            trans B (transp B B (\i -> B) b) b (f.1 a) rem2 rem1
+      in goal i
+in
+
+let not : Bool -> Bool = if (\x -> Bool) ff tt in
+
+let notInv : (b : Bool) -> Id Bool b (not (not b)) = if (\x -> Id Bool x (not (not x))) (\i -> tt) (\i -> ff) in
+
+let trueNotFalse : (A : Type) -> Id Bool tt ff -> A =
+  \A p -> comp (\i -> if (\b -> Type) (A -> A) A (p i)) i0 (\j -> []) (\x -> x) in
+
+let notEquiv : isEquiv Bool Bool not =
+  let contract1 : (a : Bool) (b : Path (\i -> Bool) tt (not a)) -> Path (\i -> fiber Bool Bool not tt) (ff, \i -> tt) (a, b)
+      = \a -> if (\a -> (b : Path (\i -> Bool) tt (not a)) -> Path (\i -> fiber Bool Bool not tt) (ff, \i -> tt) (a, b))
+                (\b -> trueNotFalse (Path (\i -> fiber Bool Bool not tt) (ff, \i -> tt) (tt, b)) b)
+                (\b i -> (ff, \j -> b (i && j)))
+                a in
+  let contract2 : (a : Bool) (b : Path (\i -> Bool) ff (not a)) -> Path (\i -> fiber Bool Bool not ff) (tt, \i -> ff) (a, b) =
+        \a -> if (\a -> (b : Path (\i -> Bool) ff (not a)) -> Path (\i -> fiber Bool Bool not ff) (tt, \i -> ff) (a, b))
+                (\b i -> (tt, \j -> b (i && j)))
+                (\b -> trueNotFalse (Path (\i -> fiber Bool Bool not ff) (tt, \i -> ff) (ff, b)) (\j -> b ~j))
+                a in
+    \b -> if (\b -> isContr (fiber Bool Bool not b))
+            ((ff, \i -> tt), \fiber -> contract1 fiber.1 fiber.2)
+            ((tt, \i -> ff), \fiber -> contract2 fiber.1 fiber.2)
+            b
+
+in the (Id Bool (not ff) tt) (\i -> transp Bool Bool (univalence Bool Bool (not, notEquiv)) ff)

src/Elab.hs

@@ -42,14 +42,9 @@ check env (P.Span s e exp) wants =
     `catch` \er -> throwIO $ InSpan s e (UnifyError er)
 
 check env exp (VSub a fm@(toFormula -> Just phi) el) = do
-  putStrLn $
-    "checking cubical subtype of " ++ show a ++ " with φ = " ++ show phi
   tm <- check env exp a
-  putStrLn $ "the expression is " ++ show tm
   for (addFormula phi env) \env -> do
     let tm' = eval env tm
-
-    putStrLn $ "have " ++ show tm'
     unifyTC env tm' el
   pure (InclSub (quote a) (quote fm) (quote el) tm)
 
@@ -95,7 +90,6 @@ check env (P.Partial fs) ty = do
     pure (fn, tn)
 
 check env exp (VPartial fm@(toFormula -> Just phi) a) = do
-  print $ (phi, a)
   case addFormula phi env of
     [] -> pure $ System (FMap mempty)
     (x:xs) -> do
@@ -115,7 +109,6 @@ check env (P.Lam s b) expected = do
       let t = Lam s I bd
           t' = eval env t
 
-      print $ (Map.lookup "phi" (names env), t', t' @@ VI0)
       checkBoundary env [s] t'
         [ ([VI0], x)
         , ([VI1], y)
@@ -230,7 +223,7 @@ infer env (P.IOr x y) = do
   y <- check env y VI
   pure (IOr x y, VI)
 
-infer env P.Path = do
+infer env P.Path =
   pure
     ( Lam "A" (quote index_t) $
         Lam "x" (App (Var "A") I0) $
@@ -240,7 +233,7 @@ infer env P.Path = do
         VPi "x" (a @@ VI0) \_ ->
           VPi "y" (a @@ VI1) (const VType))
 
-infer env P.PartialT = do
+infer env P.PartialT =
   pure
     ( Lam "r" I $
         Lam "A" Type $
@@ -248,8 +241,19 @@ infer env P.PartialT = do
     , VPi "I" VI \i ->
         VPi "A" VType (const VTypeω))
 
+infer env P.PartialP =
+  pure
+    ( Lam "r" I $
+        Lam "A" (Partial (Var "r") Typeω) $
+          PartialP (Var "r") (Var "A")
+    , VPi "phi" VI \i ->
+        VPi "A" (VPartial i VTypeω) (const VTypeω))
+
 infer env P.Comp = do
-  let u_t a r = VPi "i" VI \i -> VPartial r (a @@ i)
+  let
+    u_t a r = VPi "i" VI \i -> VPartial r (a @@ i)
+    index_t :: Value
+    index_t = VPi "_" VI (const VType)
 
   pure
     ( Lam "A" (quote index_t) $
@@ -264,7 +268,7 @@ infer env P.Comp = do
               a @@ VI1
     )
 
-infer env P.SubT = do
+infer env P.SubT =
   pure
     ( Lam "A" Type $
         Lam "phi" I $
@@ -275,6 +279,69 @@ infer env P.SubT = do
           VPi "_" (VPartial phi a) (const VType)
     )
 
+infer env P.GlueTy =
+  pure
+    ( Lam "A" Type $
+        Lam "phi" I $
+          Lam "T" (Partial (Var "phi") Type) $
+            Lam "e" (PartialP (Var "phi") (quote (equiv (VVar "T") (VVar "A")))) $
+              GlueTy (Var "A") (Var "phi") (Var "T") (Var "e")
+    , VPi "A" VType \a ->
+        VPi "phi" VI \phi ->
+          VPi "T" (VPartial phi VType) \t ->
+            VPi "e" (VPartialP phi (equiv t a)) \_ ->
+              VType
+    )
+
+infer env P.Glue =
+  pure
+    ( Lam "A" Type $
+        Lam "phi" I $
+          Lam "T" (Partial (Var "phi") Type) $
+            Lam "e" (PartialP (Var "phi") (quote (equiv (VVar "T") (VVar "A")))) $
+              Lam "t" (PartialP (Var "phi") (Var "T")) $ 
+                Lam "a" (Var "A") $
+                  Glue (Var "A") (Var "phi") (Var "T") (Var "e") (Var "t") (Var "a")
+    , VPi "A" VType \a ->
+        VPi "phi" VI \phi ->
+          VPi "T" (VPartial phi VType) \t ->
+            VPi "e" (VPartialP phi (equiv t a)) \_ ->
+              VPi "_" (VPartialP phi t) \_ ->
+                VPi "_" a \_ -> VType
+    )
+
+infer env P.Unglue =
+  pure
+    ( Lam "A" Type $
+        Lam "phi" I $
+          Lam "T" (Partial (Var "phi") Type) $
+            Lam "e" (PartialP (Var "phi") (quote (equiv (VVar "T") (VVar "A")))) $
+              Lam "g" (GlueTy (Var "A") (Var "phi") (Var "T") (Var "e")) $
+                Unglue (Var "A") (Var "phi") (Var "T") (Var "e") (Var "g")
+    , VPi "A" VType \a ->
+        VPi "phi" VI \phi ->
+          VPi "T" (VPartial phi VType) \t ->
+            VPi "e" (VPartialP phi (equiv t a)) \e ->
+              VPi "_" (VGlue a phi t e) \_ -> a
+    )
+
+infer env P.Bool = pure (Bool, VType)
+infer env P.Tt   = pure (Tt, VBool)
+infer env P.Ff   = pure (Ff, VBool)
+
+infer env P.If =
+  pure
+    (Lam "P" (Pi "_" Bool Type) $
+      Lam "x" (App (Var "P") Tt) $
+        Lam "y" (App (Var "P") Ff) $
+          Lam "b" Bool $
+            If (Var "P") (Var "x") (Var "y") (Var "b")
+    , VPi "P" (VPi "_" VBool (const VType)) \p ->
+        VPi "_" (p @@ VTrue) \_ ->
+          VPi "_" (p @@ VFalse) \_ ->
+            VPi "x" VBool \x -> p @@ x)
+
+
 infer env (P.INot x) = (, VI) . INot <$> check env x VI
 infer env P.Lam{}    = error "can't infer type for lambda"
 

src/Eval.hs

@@ -12,8 +12,6 @@ import Data.Typeable
 import Data.IORef
 import Data.Maybe
 
-import Debug.Trace
-
 import GHC.Stack
 
 import qualified Presyntax as P
@@ -24,6 +22,7 @@ import Syntax
 import System.IO.Unsafe (unsafePerformIO)
 
 import Systems
+import Debug.Trace (traceShowId)
 
 iand :: Value -> Value -> Value
 iand = \case
@@ -52,26 +51,37 @@ inot (VINot x) = x
 inot x = VINot x
 
 (@@) :: Value -> Value -> Value
-VNe hd xs @@ vl = VNe hd (PApp vl:xs)
-VLam _ _ k        @@ vl = k vl
-VEqGlued a b      @@ vl = VEqGlued (a @@ vl) (b @@ vl)
-VOfSub a phi u0 x @@ vl = x @@ vl
-VSystem fs        @@ vl = mapVSystem (VSystem fs) (@@ vl)
-f @@ _  = error $ "can't apply argument to " ++ show f
+VNe hd xs                   @@ vl = VNe hd (PApp vl:xs)
+VLam _ _ k                  @@ vl = k vl
+VEqGlued a b                @@ vl = VEqGlued (a @@ vl) (b @@ vl)
+VOfSub (VPi _ _ k) phi u0 x @@ vl = VOfSub (k vl) phi (u0 @@ vl) (x @@ vl)
+VSystem fs                  @@ vl = mapVSystem (VSystem fs) (@@ vl)
+VIf (VLam s d k) c t b      @@ vl = VIf (VLam s d (ap . force . k)) (c @@ vl) (t @@ vl) b where
+  ap (VPi _ _ r) = r vl
+  ap _ = error "type error when pushing application into if"
+f @@ _  = error $ "\ncan't apply argument to " ++ show f
 
 proj1 :: Value -> Value
 proj1 (VPair x _) = x
 proj1 (VEqGlued x y) = VEqGlued (proj1 x) (proj1 y)
 proj1 (VNe s xs) = VNe s (PProj1:xs)
 proj1 (VOfSub (VSigma _ d _) phi u0 x) = VOfSub d phi (proj1 u0) (proj1 x)
+proj1 v@VSystem{} = mapVSystem v proj1
+proj1 (VIf (VLam s d k) c t b) = VIf (VLam s d (proj1t . k)) (proj1 c) (proj1 t) b where
+  proj1t (VSigma _ d _) = d
+  proj1t _ = error "type error when pushing proj1 into if"
 proj1 x = error $ "can't proj1 " ++ show x
 
 proj2 :: Value -> Value
 proj2 (VPair _ y) = y
-proj2 (VEqGlued x y) = VEqGlued (proj1 x) (proj1 y)
+proj2 (VEqGlued x y) = VEqGlued (proj2 x) (proj2 y)
 proj2 (VNe s xs) = VNe s (PProj2:xs)
 proj2 (VOfSub (VSigma _ d r) phi u0 x) =
   VOfSub (r (proj1 x)) phi (proj2 u0) (proj2 x)
+proj2 v@VSystem{} = mapVSystem v proj2
+proj2 (VIf (VLam s d k) c t b) = VIf (VLam s d (proj2t . k)) (proj2 c) (proj2 t) b where
+  proj2t (VSigma _ d r) = r (VIf (VLam s VBool (const d)) (proj1 c) (proj1 t) b)
+  proj2t _ = error "type error when pushing proj1 into if"
 proj2 x = error $ "can't proj2 " ++ show x
 
 pathp :: Env -> Value -> Value -> Value -> Value -> Value -> Value
@@ -81,12 +91,17 @@ pathp env p x y f@(VLine _a _x _y e) i =
     Just P.Top -> VEqGlued (e i) y
     _          -> e i
 pathp env p x y (VEqGlued e e') i = VEqGlued (pathp env p x y e i) (pathp env p x y e' i)
+
 pathp env p x y (VNe hd sp) i =
   case reduceCube env i of
     Just P.Bot -> VEqGlued (VNe hd (PPathP p x y i:sp)) x
     Just P.Top -> VEqGlued (VNe hd (PPathP p x y i:sp)) y
+    _ | quote x == quote y -> VEqGlued (VNe hd (PPathP p x y i:sp)) x
     _ -> VNe hd (PPathP p x y i:sp)
+
 pathp env p x y (VOfSub _ _ _ v) i = pathp env p x y v i
+pathp env p x y v@VSystem{} i = mapVSystem v (\f -> pathp env p x y f i)
+pathp env p x y f i = error $ "Invalid pathP " ++ show f ++ " @@ " ++ show i 
 
 comp :: Env -> Value -> Formula -> Value -> Value -> Value
 comp env a@(VLam ivar VI fam) phi u a0 = glue $ go (fam (VVar "woopsie")) phi u a0 where
@@ -94,7 +109,7 @@ comp env a@(VLam ivar VI fam) phi u a0 = glue $ go (fam (VVar "woopsie")) phi u
   stuck = VComp a (toValue phi) u a0
 
   glue :: Value -> Value
-  glue = VOfSub (fam VI1) (toValue' env phi) (u @@ VI1)
+  glue = VOfSub (fam VI1) (toValue phi) (u @@ VI1)
 
   go :: HasCallStack => Value -> Formula -> Value -> Value -> Value
   go VPi{} phi u a0 =
@@ -148,6 +163,35 @@ comp env a@(VLam ivar VI fam) phi u a0 = glue $ go (fam (VVar "woopsie")) phi u
                                            ])
               (pathp env (ai0 @@ VI0) u0 v0 p0 j)
 
+  go VGlue{} psi b b0 =
+    let
+      base i    = let VGlue base _ _ _   = force $ fam i in base
+      phi i     =
+        case force (fam i) of
+          VGlue _ phi _ _    -> fromJust (reduceCube env phi)
+          x -> error (show x)
+      types i   = let VGlue _ _ types _  = force $ fam i in types
+      equivs i  = let VGlue _ _ _ equivs = force $ fam i in equivs
+
+      a i = mapVSystem (b @@ i) (unglue (base i) (phi i) (types i) (equivs i))
+      a0  = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0 
+
+      del = faceForall phi
+      a1' = comp env (VLam "i" VI base)  psi (VLam "i" VI a)      a0
+      t1' = comp env (VLam "i" VI types) psi (VLam "i" VI (b @@)) b0
+      omega   = pres env types base (flip mapVSystem proj1 . equivs) psi b b0
+      t1alpha = opEquiv env (base VI1) (types VI1) (equivs VI1) (orFormula [del, psi]) ts ps a1'
+      (t1, alpha) = (proj1 t1alpha, proj2 t1alpha)
+      
+      ts = VSystem (FMap (Map.fromList [(del, t1'), (psi, b @@ VI1)]))
+      ps = VSystem (FMap (Map.fromList [(del, omega), (psi, VLine (VLam "j" VI \_ -> base VI1) a1' a1' (\j -> a1'))]))
+
+      a1 = comp env (VLam "j" VI (const (base VI1))) (orFormula [phi VI1, psi]) (VLam "j" VI \j -> a1_sys j) a1'
+      a1_sys j = VSystem (FMap (Map.fromList [(phi VI1, pathp env (base VI1) a1' (mapVSystem (equivs VI1) proj1) alpha j), (psi, a VI1)]))
+      b1 = introGlue (base VI1) (phi VI1) (types VI1) (equivs VI1) t1 a1
+    in b1
+
+  go VBool{} _ _ a0 = a0
   go a P.Top u a0 = u @@ VI1
   go a phi u a0 = stuck
 
@@ -158,6 +202,50 @@ comp env va phi u a0 =
   where
     phi' = toValue phi
 
+opEquiv :: Env -> Value -> Value -> Value -> Formula -> Value -> Value -> Value -> Value
+opEquiv env aT tT f phi t p a = VOfSub ty (toValue phi) (VPair t p) v where
+  fun = proj1 f
+  ty  = VSigma "x" tT \x -> VPath (VLam "i" VI (const aT)) a (fun @@ x)
+  sys = Map.singleton phi (VPair t p)
+  v   = contr env ty (proj2 f @@ a) phi (VSystem (FMap sys))
+
+force :: Value -> Value
+force (VEqGlued x _) = force x
+force (VOfSub _ _ _ x) = force x
+force x = x
+
+faceForall :: (Value -> Formula) -> Formula
+faceForall k = go (k (VVar "$elim")) where
+  go (P.Is0 "$elim") = P.Bot
+  go (P.Is1 "$elim") = P.Bot
+  go (P.Or a b)      = orFormula [go a, go b]
+  go (P.And a b)     = andFormula [go a, go b]
+  go x = x
+
+pres :: Env -> (Value -> Value) -> (Value -> Value) -> (Value -> Value) -> Formula -> Value -> Value -> Value
+pres env tT tA f phi t t0 = VOfSub (VPath (tA VI1) c1 c2) (toValue phi) base (VLine (tA VI1) c1 c2 cont) where
+  c1   = comp env (VLam "i" VI tA) phi (VLam "i" VI \j -> mapVSystem t (f j @@)) (f VI0 @@ t0)
+  c2   = f VI1 @@ comp env (VLam "i" VI tA) phi t t0
+  base = VLine (tA VI1) (f VI1 @@ (t @@ VI1)) (f VI1 @@ (t @@ VI1)) (\i -> f VI1 @@ (t @@ VI1))
+  cont j =
+    let v i = fill env i tT phi t t0
+        form = orFormula [phi, fromJust (reduceCube env j)]
+        a0 = f VI0 @@ t0
+     in comp env (VLam "I" VI tA) form
+          (VLam "I" VI (\j -> VSystem (FMap (Map.fromList [(form, f j @@ v j)]))))
+          a0
+
+contr :: Env -> Value -> Value -> Formula -> Value -> Value
+contr env a aC phi u =
+  comp env (VLam "i" VI (const a)) phi
+    (VLam "i" VI (pathp env a u (proj1 aC) (proj2 aC @@ u)))
+    (proj1 aC)
+  
+-- t : Partial phi T
+-- T : Type
+-- a : A
+-- f : Equiv T A
+
 mkVSystem :: Map.Map Formula Value -> Value
 mkVSystem mp
   | Just e <- Map.lookup P.Top mp = e
@@ -189,6 +277,19 @@ evalSystem env face = mk . Map.fromList . mapMaybe (uncurry go) . Map.toList $ f
     [(_, x)] -> x
     _ -> mkVSystem x
 
+glue :: Value -> Formula -> Value -> Value -> Value
+-- glue baseT P.Top types _equivs = types
+glue baseT phi types equivs    = VGlue baseT (toValue phi) types equivs
+
+introGlue :: Value -> Formula -> Value -> Value -> Value -> Value -> Value
+introGlue baseT P.Top types equivs t a = t
+introGlue baseT phi types equivs t a = VGlueIntro baseT (toValue phi) types equivs t a
+
+unglue :: Value -> Formula -> Value -> Value -> Value -> Value
+unglue baseT P.Top types equivs b = mapVSystem equivs ((@@ b) . proj1)
+unglue baseT phi types equivs val =
+  VOfSub baseT (toValue phi) (mapVSystem equivs ((@@ val) . proj1)) (VGlueElim baseT (toValue phi) types equivs val)
+
 eval :: Env -> Term -> Value
 eval env = \case
   Var v ->
@@ -228,6 +329,7 @@ eval env = \case
 
   Path p x y      -> VPath (eval env p) (eval env x) (eval env y)
   Partial r a     -> VPartial (eval env r) (eval env a)
+  PartialP r a    -> VPartialP (eval env r) (eval env a)
 
   PathI p x y s e -> VLine (eval env p) (eval env x) (eval env y) (\ a -> eval env{ names = Map.insert s (VI, a) (names env) } e)
   PathP p x y f i -> pathp env (eval env p) (eval env x) (eval env y) (eval env f) (eval env i)
@@ -246,6 +348,50 @@ eval env = \case
 
   System fs       -> evalSystem env (getSystem fs)
 
+  GlueTy a phi types equivs ->
+    let phi' = eval env phi in
+    case reduceCube env phi' of
+      Just formula -> glue (eval env a) formula (eval env types) (eval env equivs)
+      Nothing -> VGlue (eval env a) phi' (eval env types) (eval env equivs)
+
+  Glue a phi types equivs t a0 ->
+    let phi' = eval env phi
+        t' = eval env t
+        a0' = eval env a0
+        types' = eval env types
+        equivs' = eval env equivs
+        a' = eval env a
+    in
+    case reduceCube env phi' of
+      Just formula -> introGlue a' formula types' equivs' t' a0'
+      Nothing      -> VGlueIntro a' phi' types' equivs' t' a0'
+
+  Unglue a phi types equivs val ->
+    let phi' = eval env phi
+        val' = eval env val
+        types' = eval env types
+        equivs' = eval env equivs
+        a' = eval env a
+    in
+    case reduceCube env phi' of
+      Just formula -> unglue a' formula types' equivs' val'
+      Nothing      -> VGlueElim a' phi' types' equivs' val'
+  
+  If p x y t -> elimBool (eval env p) (eval env x) (eval env y) (eval env t)
+  Tt -> VTrue
+  Ff -> VFalse
+  Bool -> VBool
+
+elimBool :: Value -> Value -> Value -> Value -> Value
+elimBool _ x _ (VEqGlued _ VTrue) = x
+elimBool _ x _ (VOfSub _ _ _ VTrue) = x
+elimBool _ x _ VTrue = x
+
+elimBool _ _ y (VEqGlued _ VFalse) = y
+elimBool _ _ y (VOfSub _ _ _ VFalse) = y
+elimBool _ _ y VFalse = y
+
+elimBool p x y t = VIf p x y t
 
 data UnifyError
   = Mismatch       Value Value
@@ -320,10 +466,12 @@ unify env (VSigma x d r) (VSigma _ d' r') = do
   unify env (r (VVar x)) (r' (VVar x))
 
 unify env VType VType = pure ()
+unify env VI  VI      = pure ()
+unify env VBool VBool = pure ()
 
-unify env VI  VI = pure ()
+unify env (VPair a b) e = unify env a (proj1 e) *> unify env b (proj2 e)
+unify env e (VPair a b) = unify env a (proj1 e) *> unify env b (proj2 e)
 
-unify env (VPair a b) (VPair c d) = unify env a c *> unify env b d
 unify env (VPath a x y) (VPath a' x' y') = unify env a a' *> unify env x x' *> unify env y y'
 unify env (VComp a phi u a0) (VComp a' phi' u' a0') =
   traverse_ (uncurry (unify env))
@@ -343,15 +491,23 @@ unify env (VSystem fs) vl
   | ((_, vl'):_) <-
       Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
   = unify env vl' vl
+  | Map.null (getSystem fs) = pure ()
 
 unify env vl (VSystem fs)
   | ((_, vl'):_) <-
     Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
   = unify env vl' vl
+  | Map.null (getSystem fs) = pure ()
 
 unify env VType VTypeω = pure ()
 unify env VTypeω VTypeω = pure ()
 
+unify env (VGlue _ VI1 b _) x = unify env b x
+
+unify env VTrue VTrue = pure ()
+unify env VFalse VFalse = pure ()
+unify env (VIf p a b c) (VIf p' a' b' c') = traverse_ (uncurry (unify env)) [(p, p'), (a, a'), (b, b'), (c, c')]
+
 unify env x y =
   case sameCube env x y of
     Just True -> pure ()
@@ -422,6 +578,10 @@ isPartialType f p@(VPartial x y) =
   case toFormula x of
     Just x -> pure (x, y)
     Nothing -> throwIO $ NotPartialType f p
+isPartialType f p@(VPartialP x y) =
+  case toFormula x of
+    Just x -> pure (x, y)
+    Nothing -> throwIO $ NotPartialType f p
 isPartialType f x = throwIO $ NotPartialType f x
 
 getVar :: IO Value
@@ -451,7 +611,7 @@ fill env i a phi u a0 =
     a0
   where
     uiand j = u @@ (i `iand` j)
-    ifc = fromJust (reduceCube env i)
+    ifc = fromMaybe P.Bot $ (reduceCube env i)
 
 toValue :: Formula -> Value
 toValue P.Top = VI1
@@ -475,8 +635,17 @@ toValue' env (P.Is0 x) =
 toValue' env (P.Is1 x) =
   case Map.lookup x (names env) of
     Just (VI, x) -> x
-    _ -> error $ "type error in toValue'"
+    vl -> error $ "type error in toValue': Is1 " ++ show x ++ ": " ++ show vl
 
 isTrue :: Value -> Bool
 isTrue VI1 = True
 isTrue _ = False
+
+equiv :: Value -> Value -> Value
+equiv t a = VSigma "f" (VPi "_" t (const a)) \f -> isEquiv t a f
+
+isEquiv :: Value -> Value -> Value -> Value
+isEquiv t a f = VPi "y" a \y -> isContr (VSigma "x" t \x -> VPath (VLam "_" VI (const a)) y (f @@ x))
+
+isContr :: Value -> Value
+isContr t = VSigma "x" t \x -> VPi "y" t \y -> VPath (VLam "_" VI (const t)) x y

src/Main.hs

@@ -20,6 +20,7 @@ import System.Console.Haskeline (runInputT, defaultSettings, getInputLine)
 import System.Exit
 
 import Systems (formulaOfFace, Face)
+import System.Environment
 
 showTypeError :: Maybe [String] -> Elab.TypeError -> String
 showTypeError lines (NotInScope l_c)       = "Variable not in scope: " ++ l_c
@@ -63,7 +64,14 @@ makeRange line (_, sc) (_, ec) = line ++ "\n" ++ replicate (sc + 1) ' ' ++ repli
 
 main :: IO ()
 main = do
-  code <- readFile "test.itt"
+  t <- getArgs
+  case t of
+    [file] -> Main.check file
+    _ -> repl
+
+check :: FilePath -> IO ()
+check file = do
+  code <- readFile file
   let
     ste e = do
       putStrLn $ showTypeError (Just (lines code)) e
@@ -72,7 +80,7 @@ main = do
     Left e -> print e
     Right x -> do
       (tm, _) <- infer (Env mempty) x `catch` ste `catch` (ste . UnifyError)
-      print tm
+      print (eval (Env mempty) tm)
 
 repl :: IO ()
 repl = runInputT defaultSettings (go (Env mempty)) where
@@ -93,7 +101,7 @@ repl = runInputT defaultSettings (go (Env mempty)) where
         Right (Assume vs) ->
           let
             loop env ((v, t):vs) = do
-              tm <- liftIO $ check env t VTypeω
+              tm <- liftIO $ Elab.check env t VTypeω
               let ty = eval env tm
               loop env{ names = Map.insert v (ty, VVar v) (names env) } vs
             loop env [] = go env
@@ -111,9 +119,9 @@ repl = runInputT defaultSettings (go (Env mempty)) where
           go env
         Right (Declare n t e) -> do
           (do
-            t <- liftIO $ check env t VTypeω
+            t <- liftIO $ Elab.check env t VTypeω
             let t' = eval env t
-            b <- liftIO $ check env e t'
+            b <- liftIO $ Elab.check env e t'
             let b' = eval env b
             go env{ names = Map.insert n (t', b') (names env) })
           `catch` \e -> (liftIO $ putStrLn (showTypeError (Just [i]) e)) *> go env

src/Presyntax.hs

@@ -30,12 +30,24 @@ data Exp
   -- Formulas, partial elements, and the type of formulas
   | Partial [(Formula, Exp)]
   | PartialT
+  | PartialP
 
   -- Compositions
   | Comp
 
   -- Cubical subtypes
   | SubT
+
+  -- Glueing
+  | GlueTy
+  | Glue
+  | Unglue
+
+  -- Bools
+  | Bool
+  | Tt
+  | Ff
+  | If
   deriving (Eq, Show, Ord)
 
 data Formula

src/Presyntax/Lexer.hs

@@ -13,7 +13,8 @@ data TokenClass
   | Tok_type
   | Tok_typeω
   | Tok_path
-  | Tok_phi
+  | Tok_Partial
+  | Tok_PartialP
   | Tok_sub
   | Tok_comp
   | Tok_tr
@@ -22,6 +23,15 @@ data TokenClass
   | Tok_I0
   | Tok_I1
 
+  | Tok_Glue
+  | Tok_glue
+  | Tok_unglue
+
+  | Tok_bool
+  | Tok_tt
+  | Tok_ff
+  | Tok_if
+
   | Tok_oparen
   | Tok_cparen
 
@@ -179,10 +189,21 @@ lexString = go 0 0 0 where
   finishIdent c
     | T.pack "Type" == c    = Tok_type
     | T.pack "Typeω" == c || T.pack "Pretype" == c = Tok_typeω
-    | T.pack "Path" == c    = Tok_path
-    | T.pack "Partial" == c = Tok_phi
-    | T.pack "Sub" == c     = Tok_sub
-    | T.pack "comp" == c    = Tok_comp
+    | T.pack "Path" == c     = Tok_path
+    | T.pack "Partial" == c  = Tok_Partial
+    | T.pack "PartialP" == c = Tok_PartialP
+    | T.pack "Sub" == c      = Tok_sub
+    | T.pack "comp" == c     = Tok_comp
+    
+    | T.pack "Glue" == c    = Tok_Glue
+    | T.pack "glue" == c    = Tok_glue
+    | T.pack "unglue" == c  = Tok_unglue
+
+    | T.pack "Bool" == c    = Tok_bool
+    | T.pack "tt" == c      = Tok_tt
+    | T.pack "ff" == c      = Tok_ff
+    | T.pack "if" == c      = Tok_if
+    
     | T.pack "tr" == c      = Tok_tr
     | T.pack "I" == c       = Tok_I
     | T.pack "i0" == c      = Tok_I0

src/Presyntax/Parser.hs

@@ -185,18 +185,36 @@ exprConj = attachPos $
 atom0 :: Parser Exp
 atom0 = attachPos $
        fmap (Var . T.unpack) var
-   <|> fmap (const Type)     (expect Tok_type)
-   <|> fmap (const Typeω)    (expect Tok_typeω)
-   <|> fmap (const I)        (expect Tok_I)
-   <|> fmap (const I0)       (expect Tok_I0)
-   <|> fmap (const I1)       (expect Tok_I1)
-   <|> fmap (const Path)     (expect Tok_path)
-   <|> fmap (const SubT)     (expect Tok_sub)
-   <|> fmap (const PartialT) (expect Tok_phi)
-   <|> fmap (const Comp)     (expect Tok_comp)
-   <|> fmap INot           (expect Tok_not *> atom)
+   <|> keywords
+   <|> fmap INot             (expect Tok_not *> atom)
    <|> parens pair
    <|> square (Partial <$> (system <|> pure []))
+  where
+    table = [ (Type,      Tok_type)
+            , (Typeω,     Tok_typeω)
+            , (I,         Tok_I)
+            , (I0,        Tok_I0)
+            , (I1,        Tok_I1)
+            , (Path,      Tok_path)
+            , (SubT,      Tok_sub)
+            , (PartialT,  Tok_Partial)
+            , (PartialP,  Tok_PartialP)
+
+            , (Comp,      Tok_comp)
+            , (SubT,      Tok_sub)
+            , (Comp,      Tok_comp)
+
+            , (GlueTy,    Tok_Glue)
+            , (Glue,      Tok_glue)
+            , (Unglue,    Tok_unglue)
+
+            , (Bool,      Tok_bool)
+            , (Tt,        Tok_tt)
+            , (Ff,        Tok_ff)
+            , (If,        Tok_if)
+            ]
+    keyword (x, y) = fmap (const x) (expect y)
+    keywords = foldr ((<|>) . keyword) empty table
 
 atom :: Parser Exp
 atom = attachPos $
@@ -282,3 +300,4 @@ formula = conjunction where
      <|> (Is0 . T.unpack) <$> (expect Tok_not *> var)
      <|> Top <$ expect Tok_I1
      <|> Bot <$ expect Tok_I0
+     <|> parens conjunction

src/Syntax.hs

@@ -42,9 +42,33 @@ data Term
 
   | System (System Term)
   | Partial Term Term
+  | PartialP Term Term
   | Comp Term Term Term Term
   | Sub Term Term Term
   | InclSub Term Term Term Term
+
+  | GlueTy
+      Term -- Base type
+      Term -- Extent
+      Term -- Partial types
+      Term -- Partial equivs
+  | Glue
+      Term -- Base
+      Term -- Extent
+      Term -- Partial types
+      Term -- Partial equivs
+      Term -- t
+      Term -- a
+  | Unglue
+      Term -- Base
+      Term -- Extent
+      Term -- Partial types
+      Term -- Partial equivs
+      Term -- glued value
+    
+  | Bool
+  | Tt | Ff
+  | If Term Term Term Term
   deriving (Eq, Ord)
 
 instance Show Term where
@@ -53,13 +77,17 @@ instance Show Term where
       Var s -> showString s
       System fs -> showListWith showPE (Map.toList (getSystem fs))
       -- ew
-      App (App (App (Lam _ _ (Lam _ _ (Lam _ _ Path{}))) a) x) y -> showsPrec p (Path a x y)
-      App (App (App (Lam _ _ (Lam _ _ (Lam _ _ Sub{}))) a) x) y -> showsPrec p (Sub a x y)
-      App (App (Lam _ _ (Lam _ _ Partial{})) phi) r -> showsPrec p (Partial phi r)
+      App (App (App (Lam _ _ (Lam _ _ (Lam _ _ Path{}))) a) x) y   -> showsPrec p (Path a x y)
+      App (App (App (Lam _ _ (Lam _ _ (Lam _ _ Sub{}))) a) x) y    -> showsPrec p (Sub a x y)
+      App (App (Lam _ _ (Lam _ _ Partial{})) phi) r                -> showsPrec p (Partial phi r)
+      App (App (Lam _ _ (Lam _ _ PartialP{})) phi) r               -> showsPrec p (PartialP phi r)
 
       App (App (App (App (Lam _ _ (Lam _ _ (Lam _ _ (Lam _ _ Comp{})))) a) phi) u) a0 ->
         showsPrec p (Comp a phi u a0)
 
+      App (App (App (App (Lam _ _ (Lam _ _ (Lam _ _ (Lam _ _ GlueTy{})))) a) phi) u) a0 ->
+        showsPrec p (GlueTy a phi u a0)
+
       App f x -> showParen (p >= app_prec) $
         showsPrec fun_prec f
         . showChar ' '
@@ -131,13 +159,27 @@ instance Show Term where
 
       INot s -> showChar '~' . showsPrec p s
 
-      Path a x y -> showsPrec p (App (App (App (Var "Path") a) x) y)
-      Sub a x y -> showsPrec p (App (App (App (Var "Sub") a) x) y)
-      Partial r a -> showsPrec p (App (App (Var "Partial") r) a)
+      Path a x y       -> showApps p (Var "Path") [a, x, y]
+      Sub a x y        -> showApps p (Var "Sub") [a, x, y]
       InclSub _a _phi _u0 a0 -> showsPrec p a0
 
-      Comp a I0 (Lam _ I (System (FMap (Map.null -> True)))) a0 -> showsPrec p (foldl App (Var "transp") [a, a0])
-      Comp a phi u a0 -> showsPrec p (foldl App (Var "comp") [a, phi, u, a0])
+      GlueTy a phi t e -> showApps p (Var "Glue") [a, phi, t, e]
+      Glue base phi ty te t a ->
+        showApps p (Var "glue") [phi, t, a]
+      Unglue base phi ty te a ->
+        showApps p (Var "unglue") [a]
+
+      Partial r a -> showApps p (Var "Partial") [r, a]
+      PartialP r a -> showApps p (Var "PartialP") [r, a]
+
+      Comp a phi u a0 -> showApps p (Var "comp") [a, phi, u, a0]
+
+      If _ Ff Tt d -> showApps p (Var "not") [d]
+      If _ b c d -> showApps p (Var "if") [b, c, d]
+
+      Bool -> showString "Bool"
+      Tt -> showString "tt"
+      Ff -> showString "ff"
 
       PathI a x y s b -> showParen (p >= fun_prec) $
         showString ("λ " ++ s ++ " -> ")
@@ -163,6 +205,9 @@ instance Show Term where
       or_prec     = 3
       fun_prec    = 1
 
+showApps :: Int -> Term -> [Term] -> ShowS
+showApps p f xs = showsPrec p (foldl App f xs)
+
 showPE :: (Formula, Term) -> String -> String
 showPE (f, t) = shows f . showString " -> " . shows t
 
@@ -188,8 +233,18 @@ data Value
   | VPath Value Value Value
   | VSub Value Value Value
   | VPartial Value Value
+  | VPartialP Value Value
   | VComp Value Value Value Value
 
+  | VGlue      Value Value Value Value
+  | VGlueIntro Value Value Value Value Value Value
+  | VGlueElim  Value Value Value Value Value 
+
+  | VBool
+  | VTrue
+  | VFalse
+  | VIf Value Value Value Value
+
 data Proj
   = PApp Value
   | PPathP Value Value Value Value
@@ -227,6 +282,7 @@ quote = go mempty where
   go scope (VPath a x y) = Path (go scope a) (go scope x) (go scope y)
   go scope (VSub a x y) = Sub (go scope a) (go scope x) (go scope y)
   go scope (VPartial r a) = Partial (go scope r) (go scope a)
+  go scope (VPartialP r a) = PartialP (go scope r) (go scope a)
   go scope (VComp a b c d) = Comp (go scope a) (go scope b) (go scope c) (go scope d)
 
   go scope (VEqGlued e _) = go scope e
@@ -237,6 +293,17 @@ quote = go mempty where
   go scope (VSystem (FMap fs)) = System (FMap (fmap (go scope) fs))
   go scope (VOfSub _ _ _ x) = go scope x
 
+  go scope (VGlue a phi tys eqvs) = GlueTy (go scope a) (go scope phi) (go scope tys) (go scope eqvs)
+  go scope (VGlueIntro base phi tys eqvs t a) =
+    Glue (go scope base) (go scope phi) (go scope tys) (go scope eqvs) (go scope t) (go scope a)
+  go scope (VGlueElim base phi tys eqvs a) =
+    Unglue (go scope base) (go scope phi) (go scope tys) (go scope eqvs) (go scope a)
+
+  go scope VBool = Bool
+  go scope VTrue = Tt
+  go scope VFalse = Ff
+  go scope (VIf a b c d) = If (go scope a) (go scope b) (go scope c) (go scope d)
+
   goSpine :: Set String -> Term -> Proj -> Term
   goSpine scope t (PApp x) = App t (go scope x)
   goSpine scope t (PPathP a x y i) = PathP (go scope a) (go scope x) (go scope y) t (go scope i)

src/Systems.hs

@@ -94,4 +94,4 @@ emptySystem :: System a
 emptySystem = FMap mempty
 
 mapSystem :: System a -> (a -> b) -> System b
-mapSystem (FMap x) f = FMap (fmap f x)
+mapSystem (FMap x) f = FMap (Map.filterWithKey (\f _ -> f /= Bot) (fmap f x))

test.itt

@@ -1,79 +0,0 @@
-{- {- let
-  sym : (A : Type) (x y : A) -> Path (\x -> A) x y -> Path (\x -> A) y x
-    = λ A x y p i -> p (~ i)
-in let
-  funext : (A : Type) (B : A -> Type) (f g : (x : A) -> B x) -> ((x : A) -> Path (\i -> B x) (f x) (g x)) -> Path (\i -> (x : A) -> B x) f g
-    = λ A B f g h i x -> h x i
-in let
-  i0IsI1 : Path (\x -> I) i0 i1
-    = λ i -> i
-in let
-  singContr : (A : Type) (a b : A) (p : Path (\j -> A) a b) -> Path (\i -> (x : A) * (Path (\j -> A) a x)) (a, \i -> a) (b, p)
-    = λ A a b p i -> (p i, λ j -> p (i && j))
-in let
-  transport : (A : I -> Type) (a : A i0) -> A i1
-    = \A a -> comp A i0 (\i -> []) a
-in let
-  Jay : (A : Type) (x : A)
-        (P : (y : A) -> Path (\i -> A) x y -> Type)
-        (d : P x (\i -> x))
-        (y : A) (p : Path (\i -> A) x y)
-     -> P y p
-    = \A x P d y p -> transport (\i -> P (p i) (\j -> p (i && j))) d
-in -}
-let
-  fill : (i : I) (A : I -> Type)
-         (phi : I) (u : (i : I) -> Partial phi (A i))
-      -> Sub (A i0) phi (u i0) -> A i
-    = \i A phi u a0 ->
-      comp (\j -> A (i && j)) (phi || ~i) (\j -> [ phi -> u (i && j), ~i -> a0 ]) a0
-in let
-  trans : (A : Type) (a b c : A)
-       -> Path (\i -> A) a b
-       -> Path (\i -> A) b c
-       -> Path (\i -> A) a c
-    = \A a b c p q i ->
-      comp (\j -> A) (i || ~i)
-           (\j -> [ ~i -> a, i -> q j ])
-           (p i)
-in let
-  elimI : (P : I -> Type)
-          (a : P i0)
-          (b : P i1)
-       -> Path P a b
-       -> (i : I) -> P i
-    = \P a b p i -> p i
-in let
-  contrI : (i : I) -> Path (\i -> I) i0 i
-    = \i -> elimI (\x -> Path (\i -> I) i0 x) (\i -> i0) (\i -> i) (\i j -> i && j) i
-in let
-  IisContr : (i : I) * ((j : I) -> Path (\i -> I) i j)
-    = (i0, contrI)
-in let
-  compPath : (A : I -> Type)
-             (phi : I) (u : (i : I) -> Partial phi (A i))
-          -> (a0 : Sub (A i0) phi (u i0)) -> Path A a0 (comp A phi u a0)
-    = \A phi u a0 j -> fill j A phi u a0
-in compPath -}
-
-let
-  fill : (i : I) (A : I -> Type)
-         (phi : I) (u : (i : I) -> Partial phi (A i))
-      -> Sub (A i0) phi (u i0) -> A i
-    = \i A phi u a0 ->
-      comp (\j -> A (i && j)) (phi || ~i) (\j -> [ phi -> u (i && j), ~i -> a0 ]) a0
-in 
-let
-  pres : (A : I -> Type)
-         (T : I -> Type)
-         (f : (i : I) -> T i -> A i)
-         (phi : I)
-         (t : (i : I) -> Partial phi (T i))
-         (t0 : Sub (T i0) phi (t i0))
-      -> (let c1 : A i1 = comp A phi (\j -> [phi -> f j (t j)]) (f i0 t0) in
-          let c2 : A i1 = f i1 (comp T phi (\j -> [phi -> t j]) t0) in
-            Sub (Path (\i -> A i1) c1 c2) phi (\j -> f i1 (t i1)))
-  = \A T f phi t t0 j ->
-      let v : (i : I) -> T i = \i -> fill i T phi (\j -> [phi -> t j]) t0
-       in comp A (phi || j) (\u -> [phi || j -> f u (v u)]) (f i0 t0)
-in pres