organize imports

src/Elab.hs

@@ -6,19 +6,22 @@
 module Elab where
 
 import Control.Exception
+import Control.Monad
 
 import qualified Data.Map.Strict as Map
+import qualified Data.Set as Set
+import Data.Traversable
+import Data.Set (Set)
 import Data.Typeable
+import Data.Foldable
+
+import Eval
 
 import qualified Presyntax as P
+
 import Syntax
-import Eval
-import Control.Monad
+
 import Systems
-import Data.Traversable
-import qualified Data.Set as Set
-import Data.Set (Set)
-import Data.Foldable
 
 data TypeError
   = NotInScope String
@@ -36,32 +39,19 @@ check env (P.Span s e exp) wants =
     `catch` \case
       InSpan s e err -> throwIO $ InSpan s e err
       err -> throwIO $ InSpan s e err
+    `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
-  for (addFormula phi env) \env -> 
+  putStrLn $ "the expression is " ++ show tm
+  for (addFormula phi env) \env -> do
     let tm' = eval env tm
-     in unifyTC env tm' el
-  pure (InclSub (quote a) (quote fm) (quote el) tm)
-
-check env (P.Lam s b) expected = do
-  expc <- isPiOrPathType expected
-  case expc of
-    Left (_, d, r) -> do -- function
-      bd <- check env { names = Map.insert s (makeValueGluingSub d s) (names env) } b (r (VVar s))
-      pure (Lam s (quote d) bd)
-    Right (a, x, y) -> do
-      bd <- check env { names = Map.insert s (VI, VVar s) (names env) } b (a @@ VVar s)
 
-      let t = Lam s I bd
-          t' = eval env t
-
-      checkBoundary env [s] t'
-        [ ([VI0], x)
-        , ([VI1], y)
-        ]
-
-      pure (PathI (quote a) (quote x) (quote y) s bd)
+    putStrLn $ "have " ++ show tm'
+    unifyTC env tm' el
+  pure (InclSub (quote a) (quote fm) (quote el) tm)
 
 check env (P.Let v t d b) expected = do
   ty <- check env t VTypeω
@@ -98,12 +88,41 @@ check env (P.Partial fs) ty = do
 
   fmap (System . FMap . Map.fromList) $ for ts \(fn, tn) -> do
     for ts \(fm, tm) -> do
-      when (possible (fn `P.And` fm)) do
+      when (fn /= fm && possible (fn `P.And` fm)) do
         for_ (addFormula (fn `P.And` fm) env) $ \env ->
           unifyTC (env) (eval env tn) (eval env tm)
             `catch` \e -> throwIO (IncompatibleFaces (fn, tn) (fm, tm) e)
     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
+      tm <- check x exp a
+      for_ xs $ \e -> check e exp a
+      pure tm
+
+check env (P.Lam s b) expected = do
+  expc <- isPiOrPathType expected
+  case expc of
+    Left (_, d, r) -> do -- function
+      bd <- check env { names = Map.insert s (makeValueGluingSub d s) (names env) } b (r (VVar s))
+      pure (Lam s (quote d) bd)
+    Right (a, x, y) -> do
+      bd <- check env { names = Map.insert s (VI, VVar s) (names env) } b (a @@ VVar s)
+
+      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)
+        ]
+
+      pure (PathI (quote a) (quote x) (quote y) s bd)
+
 check env exp expected = do
   (term, actual) <- infer env exp
   unifyTC env actual expected
@@ -134,7 +153,7 @@ checkBoundary env ns f = finish <=< go where
     case t of
       Right _ -> go faces
       Left e -> ((ixs, vl, e):) <$> go faces
-  
+
   finish [] = pure ()
   finish xs = throwIO $ WrongFaces f xs
 
@@ -144,6 +163,7 @@ infer env (P.Span s e exp) =
     `catch` \case
       InSpan s e err -> throwIO $ InSpan s e err
       err -> throwIO $ InSpan s e err
+    `catch` \er -> throwIO $ InSpan s e (UnifyError er)
 
 infer env (P.Var s) =
   case Map.lookup s (names env) of
@@ -170,7 +190,8 @@ infer env (P.Pi s d r) = do
     VTypeω -> pure VTypeω
     _ -> throwIO . UnifyError $ NotSort ty
   let d' = eval env dom
-  (rng, rng_t) <- infer env { names = Map.insert s (d', VVar s) (names env) } r
+  (rng, rng_t) <-
+    infer env { names = Map.insert s (makeValueGluingSub d' s) (names env) } r
   case ty of
     VType -> pure VType
     VTypeω -> pure VTypeω
@@ -269,7 +290,7 @@ infer env (P.Proj1 x) = do
   (t, ty) <- infer env x
   (_, d, _) <- isSigmaType ty
   pure (Proj1 t, d)
-  
+
 infer env (P.Proj2 x) = do
   (t, ty) <- infer env x
   let t' = eval env t

src/Eval.hs

@@ -4,20 +4,27 @@
 {-# LANGUAGE LambdaCase #-}
 module Eval where
 
-import Syntax
+import Control.Exception
+
 import qualified Data.Map.Strict as Map
 import Data.Foldable
-import Control.Exception
 import Data.Typeable
-import System.IO.Unsafe (unsafePerformIO)
 import Data.IORef
-import Systems
-import Presyntax (Formula)
-import qualified Presyntax as P
 import Data.Maybe
+
 import Debug.Trace
+
 import GHC.Stack
 
+import qualified Presyntax as P
+import Presyntax (Formula)
+
+import Syntax
+
+import System.IO.Unsafe (unsafePerformIO)
+
+import Systems
+
 iand :: Value -> Value -> Value
 iand = \case
   VI1 -> id
@@ -82,16 +89,12 @@ pathp env p x y (VNe hd sp) i =
 pathp env p x y (VOfSub _ _ _ v) i = pathp env p x y v i
 
 comp :: Env -> Value -> Formula -> Value -> Value -> Value
-comp env a@(VLam ivar VI fam) phi u a0 = go (fam (VVar "woopsie")) phi u a0 where
-  i = VVar ivar
+comp env a@(VLam ivar VI fam) phi u a0 = glue $ go (fam (VVar "woopsie")) phi u a0 where
   stuck :: Value
-  stuck = maybeAddEq $ VComp a (toValue phi) u a0
+  stuck = VComp a (toValue phi) u a0
 
-  maybeAddEq :: Value -> Value
-  maybeAddEq =
-    if phi == P.Top
-      then flip VEqGlued (u @@ VI1)
-      else id
+  glue :: Value -> Value
+  glue = VOfSub (fam VI1) (toValue' env phi) (u @@ VI1)
 
   go :: HasCallStack => Value -> Formula -> Value -> Value -> Value
   go VPi{} phi u a0 =
@@ -106,7 +109,7 @@ comp env a@(VLam ivar VI fam) phi u a0 = go (fam (VVar "woopsie")) phi u a0 wher
        comp env
         (VLam ivar VI (\i -> rng i (ybar i arg)))
         phi
-        (VLam "i" VI \i -> mapVSystem (u @@ i) (@@ ybar i arg)) 
+        (VLam "i" VI \i -> mapVSystem (u @@ i) (@@ ybar i arg))
         (a0 @@ ybar VI0 arg)
 
   go VSigma{} phi u a0 =
@@ -146,7 +149,7 @@ comp env a@(VLam ivar VI fam) phi u a0 = go (fam (VVar "woopsie")) phi u a0 wher
               (pathp env (ai0 @@ VI0) u0 v0 p0 j)
 
   go a P.Top u a0 = u @@ VI1
-  go a phi u a0 = maybeAddEq stuck
+  go a phi u a0 = stuck
 
 comp env va phi u a0 =
   if phi == P.Top
@@ -171,21 +174,16 @@ mapVSystem (VSystem ss) f = VSystem (mapSystem ss f)
 mapVSystem x f = f x
 
 evalSystem :: Env -> Map.Map Formula Term -> Value
-evalSystem env face = mk . Map.mapMaybeWithKey go $ face where
-  go :: Formula -> Term -> Maybe Value
+evalSystem env face = mk . Map.fromList . mapMaybe (uncurry go) . Map.toList $ face where
+  go :: Formula -> Term -> Maybe (Formula, Value)
   go face tm
     | VI0 <- toValue' env face = Nothing
-    | otherwise = Just (eval env tm)
+    | otherwise = Just (evalF env face, eval env tm)
 
-  differsFromEnv :: String -> Bool -> Bool
-  differsFromEnv x True =
-    case Map.lookup x (names env) of
-      Just (VI, VI0) -> True
-      _ -> False
-  differsFromEnv x False =
-    case Map.lookup x (names env) of
-      Just (VI, VI1) -> True
-      _ -> False
+  evalF env tm =
+    case toFormula (toValue' env tm) of
+      Just f -> f
+      Nothing -> error $ "eval turned formula into non formula"
 
   mk x = case Map.toList x of
     [(_, x)] -> x
@@ -222,6 +220,7 @@ eval env = \case
   Proj2 y  -> proj2 (eval env y)
 
   Type     -> VType
+  Typeω    -> VTypeω
 
   I   -> VI
   I0  -> VI0
@@ -236,9 +235,9 @@ eval env = \case
   Sub p x y          -> VSub (eval env p) (eval env x) (eval env y)
   InclSub a phi u a0 -> VOfSub (eval env a) (eval env phi) (eval env u) (eval env a0)
 
-  IAnd x y        -> iand (eval env x) (eval env y)
-  IOr x y         -> ior (eval env x) (eval env y)
-  INot x          -> inot (eval env x)
+  IAnd x y  -> iand (eval env x) (eval env y)
+  IOr x y   -> ior (eval env x) (eval env y)
+  INot x    -> inot (eval env x)
 
   Comp a phi u a0 ->
     case reduceCube env (eval env phi) of
@@ -256,14 +255,18 @@ data UnifyError
   | NotSort        Value
   deriving (Show, Typeable, Exception)
 
-unify :: Env -> Value -> Value -> IO ()
+unify :: HasCallStack => Env -> Value -> Value -> IO ()
 unify env (VEqGlued a b) c =
   unify env a c `catch` \e -> const (unify env b c) (e :: UnifyError)
 unify env c (VEqGlued a b) =
   unify env c a `catch` \e -> const (unify env c b) (e :: UnifyError)
 
-unify env (VLine a x y f) e = unify env (f (VVar "i")) (pathp env a x y e (VVar "i"))
-unify env e (VLine a x y f) = unify env (f (VVar "i")) (pathp env a x y e (VVar "i"))
+unify env (VLine a x y f) e =
+  let env' = env { names = Map.insert "i" (VI, VVar "i") (names env) }
+   in unify env' (f (VVar "i")) (pathp env' a x y e (VVar "i"))
+unify env e (VLine a x y f) =
+  let env' = env { names = Map.insert "i" (VI, VVar "i") (names env) }
+   in unify env' (f (VVar "i")) (pathp env' a x y e (VVar "i"))
 
 unify env (VPartial r b) (VPartial r' b') = do
   unify env b b'
@@ -303,6 +306,7 @@ unify env vl1@(VNe x sp) vl2@(VNe y sp')
     unifySp (PPathP _a _x _y i) (PPathP _a' _x' _y' i') = unify env i i'
     unifySp PProj1 PProj1 = pure ()
     unifySp PProj2 PProj2 = pure ()
+    unifySp _ _ = throwIO $ Mismatch vl1 vl2
 
 unify env (VLam x _ k) e = unify env (k (VVar x)) (e @@ VVar x)
 unify env e (VLam x _ k) = unify env (e @@ VVar x) (k (VVar x))
@@ -321,13 +325,28 @@ unify env VI  VI = pure ()
 
 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))
+    [ (a, a')
+    , (phi, phi')
+    , (u, u')
+    , (a0, a0')
+    ]
+
+unify env (VComp a (reduceCube env -> Just P.Top) u a0) vl =
+  unify env (u @@ VI1) vl
+
+unify env vl (VComp a (reduceCube env -> Just P.Top) u a0) =
+  unify env (u @@ VI1) vl
 
 unify env (VSystem fs) vl
-  | ((_, vl'):_) <- Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
+  | ((_, vl'):_) <-
+      Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
   = unify env vl' vl
 
 unify env vl (VSystem fs)
-  | ((_, vl'):_) <- Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
+  | ((_, vl'):_) <-
+    Map.toList (Map.filterWithKey (\f _ -> isTrue (toValue' env f)) (getSystem fs))
   = unify env vl' vl
 
 unify env VType VTypeω = pure ()
@@ -350,7 +369,7 @@ reduceCube env x = fmap (toDNF . simplify) (toFormula x) where
     case Map.lookup x (names env) of
       Just (VI, VI1) -> P.Top
       Just (VI, VI0) -> P.Bot
-      _ -> P.Is0 x
+      _ -> P.Is1 x
   simplify (P.And x y) = P.And (simplify x) (simplify y)
   simplify (P.Or x y) = P.Or (simplify x) (simplify y)
   simplify x = x
@@ -362,10 +381,10 @@ sameCube env x y =
     _ -> Nothing
 
 toFormula :: Value -> Maybe Formula
-toFormula VI0                = Just P.Bot
-toFormula VI1                = Just P.Top
+toFormula VI0         = Just P.Bot
+toFormula VI1         = Just P.Top
 toFormula (VNe x [])  = Just (P.Is1 x)
-toFormula (VINot f)    = notFormula <$> toFormula f
+toFormula (VINot f)   = notFormula <$> toFormula f
 toFormula (VIAnd x y) = do
   s <- toFormula y
   t <- toFormula x
@@ -442,7 +461,7 @@ toValue (P.Or x y) = toValue x `ior` toValue y
 toValue (P.Is0 x) = inot (VVar x)
 toValue (P.Is1 x) = VVar x
 
-toValue' :: Env -> Formula -> Value
+toValue' :: HasCallStack => Env -> Formula -> Value
 toValue' env P.Top = VI1
 toValue' env P.Bot = VI0
 toValue' env (P.And x y) = toValue x `iand` toValue y
@@ -452,7 +471,7 @@ toValue' env (P.Is0 x) =
     Just (VI, VI0) -> VI1
     Just (VI, VI1) -> VI0
     Just (VI, x) -> inot x
-    _ -> error $ "type error in toValue'"
+    vl -> error $ "type error in toValue' " ++ x ++ ": " ++ show vl
 toValue' env (P.Is1 x) =
   case Map.lookup x (names env) of
     Just (VI, x) -> x

src/Main.hs

@@ -1,18 +1,25 @@
 {-# LANGUAGE LambdaCase #-}
 module Main where
 
-import Presyntax.Parser
-import Elab
-import Control.Monad.Catch
-import System.Exit
-import Syntax
-import System.Console.Haskeline (runInputT, defaultSettings, getInputLine)
 import Control.Monad.IO.Class
-import Presyntax
+import Control.Monad.Catch
+
 import qualified Data.Map.Strict as Map
+import Data.List
+
+import Elab
+
 import Eval (eval, UnifyError (..))
+
+import Presyntax.Parser
+import Presyntax
+
+import Syntax
+
+import System.Console.Haskeline (runInputT, defaultSettings, getInputLine)
+import System.Exit
+
 import Systems (formulaOfFace, Face)
-import Data.List
 
 showTypeError :: Maybe [String] -> Elab.TypeError -> String
 showTypeError lines (NotInScope l_c)       = "Variable not in scope: " ++ l_c
@@ -37,7 +44,7 @@ showTypeError lines (InSpan start end err)
   | otherwise = showTypeError Nothing err
 
 showTypeError lines (IncompleteSystem formula extent) =
-  unlines $ 
+  unlines $
     [ "Incomplete system: "
     , "it is defined by " ++ show formula
     , "but the context mandates extent " ++ show extent ]
@@ -57,12 +64,14 @@ makeRange line (_, sc) (_, ec) = line ++ "\n" ++ replicate (sc + 1) ' ' ++ repli
 main :: IO ()
 main = do
   code <- readFile "test.itt"
+  let
+    ste e = do
+      putStrLn $ showTypeError (Just (lines code)) e
+      exitFailure
   case parseString body code of
     Left e -> print e
     Right x -> do
-      (tm, _) <- infer (Env mempty ) x `catch` \e -> do
-        putStrLn $ showTypeError (Just (lines code)) e
-        exitFailure
+      (tm, _) <- infer (Env mempty) x `catch` ste `catch` (ste . UnifyError)
       print tm
 
 repl :: IO ()
@@ -70,7 +79,7 @@ repl = runInputT defaultSettings (go (Env mempty)) where
   go env = getInputLine "> " >>= \case
     Just i | ":sq " `isPrefixOf` i -> do
       case parseString body (replicate 4 ' ' ++ drop 4 i) of
-        Right exp -> 
+        Right exp ->
           (do
             (tm, ty) <- liftIO $ infer env exp
             liftIO $ drawExtent ty (eval env tm)
@@ -102,7 +111,7 @@ repl = runInputT defaultSettings (go (Env mempty)) where
           go env
         Right (Declare n t e) -> do
           (do
-            t <- liftIO $ check env t VType
+            t <- liftIO $ check env t VTypeω
             let t' = eval env t
             b <- liftIO $ check env e t'
             let b' = eval env b
@@ -120,7 +129,7 @@ drawExtent ty vl = nicely $ getDirections ty vl where
     in map (\(p, t, v) -> ((s, True):p, t, v))  trues
     ++ map (\(p, t, v) -> ((s, False):p, t, v)) falses
   getDirections ty t = [([], ty, t)]
-  
+
   nicely :: [([(String, Bool)], Value, Value)] -> IO ()
   nicely [] = pure ()
   nicely ((bs, ty, el):fcs) = do
@@ -131,4 +140,4 @@ drawExtent ty vl = nicely $ getDirections ty vl where
   theFace = map (\(i, b) ->
     if b
       then "(" ++ i ++ "1)"
-      else "(" ++ i ++ "0)")
+      else "(" ++ i ++ "0)")

src/Presyntax.hs

@@ -33,7 +33,7 @@ data Exp
 
   -- Compositions
   | Comp
-  
+
   -- Cubical subtypes
   | SubT
   deriving (Eq, Show, Ord)
@@ -69,4 +69,4 @@ instance Show Formula where
 data Statement
   = Assume [(String, Exp)]
   | Declare String Exp Exp
-  | Eval Exp
+  | Eval Exp

src/Presyntax/Lexer.hs

@@ -1,10 +1,9 @@
 {-# LANGUAGE BangPatterns #-}
 module Presyntax.Lexer where
 
+import qualified Data.Text as T
 import Data.Text (Text)
-
 import Data.Char
-import qualified Data.Text as T
 
 {- HLINT ignore -}
 data TokenClass
@@ -28,7 +27,7 @@ data TokenClass
 
   | Tok_osquare
   | Tok_csquare
-  
+
   | Tok_colon
   | Tok_arrow
 
@@ -82,7 +81,7 @@ lexString = go 0 0 0 where
   go !off !line !_ ('-':'-':xs) =
     let (a, b) = span (/= '\n') xs
      in go (off + length a) line 0 b
-  
+
   go !off !line !col ('{':'-':xs) = skipComment off line col 1 xs
 
   go !off !line !col ('~':cs) =
@@ -179,7 +178,7 @@ lexString = go 0 0 0 where
 
   finishIdent c
     | T.pack "Type" == c    = Tok_type
-    | 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
@@ -191,4 +190,4 @@ lexString = go 0 0 0 where
     | T.pack "let" == c     = Tok_let
     | T.pack "in" == c      = Tok_in
     | T.pack "assume" == c  = Tok_assume
-    | otherwise             = Tok_var c
+    | otherwise             = Tok_var c

src/Presyntax/Parser.hs

@@ -13,7 +13,6 @@ import Data.Text (Text)
 import Presyntax.Lexer
 import Presyntax
 
-
 data ParseError
   = UnexpectedEof Int Int
   | Unexpected Token
@@ -187,6 +186,7 @@ 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)
@@ -281,4 +281,4 @@ formula = conjunction where
   atom = (Is1 . T.unpack) <$> var
      <|> (Is0 . T.unpack) <$> (expect Tok_not *> var)
      <|> Top <$ expect Tok_I1
-     <|> Bot <$ expect Tok_I0
+     <|> Bot <$ expect Tok_I0

src/Syntax.hs

@@ -3,13 +3,16 @@
 {-# LANGUAGE PatternSynonyms #-}
 module Syntax where
 
-import Data.Set (Set)
+import qualified Data.Map.Strict as Map
 import qualified Data.Set as Set
 import Data.Map.Strict (Map)
+import Data.Set (Set)
+
+import Presyntax (Formula)
+
 import Systems
-import qualified Data.Map.Strict as Map
+
 import Text.Show (showListWith)
-import Presyntax (Formula)
 
 type Space = Term
 
@@ -99,7 +102,7 @@ instance Show Term where
             . showString " -> "
             . shows r
           showBinder (Pi n d r) =
-            let 
+            let
               arr = case r of
                 Pi n _ _ | n /= "_" -> " "
                 _ -> " -> "

src/Systems.hs

@@ -1,12 +1,13 @@
 module Systems where
 
-import Data.Map.Strict (Map)
-import Presyntax
 import qualified Data.Map.Strict as Map
-import Data.Set (Set)
 import qualified Data.Set as Set
+import Data.Map.Strict (Map)
+import Data.Set (Set)
 import Data.List
 
+import Presyntax
+
 newtype Face = Face { getFace :: Map String Bool }
   deriving (Eq, Show, Ord)
 
@@ -40,7 +41,7 @@ faces formula = partition (evalFormula formula) allPossible where
   truths []     = [mempty]
   truths (x:xs) = uncurry Map.insert <$> [(x, True), (x, False)] <*> truths xs
 
-  allPossible = Face <$> truths (Set.toList (freeVarsFormula formula)) 
+  allPossible = Face <$> truths (Set.toList (freeVarsFormula formula))
 
 impossible, possible, tautological :: Formula -> Bool
 impossible = null . fst . faces
@@ -48,7 +49,7 @@ possible = not . null . fst . faces
 tautological = not . null . snd . faces
 
 toDNF :: Formula -> Formula
-toDNF = orFormula . map formulaOfFace . fst . faces 
+toDNF = orFormula . map formulaOfFace . fst . faces
 
 formulaOfFace :: Face -> Formula
 formulaOfFace = andFormula . map (\(x, i) -> if i then Is1 x else Is0 x) . Map.toDescList . getFace
@@ -93,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 (fmap f x)

test.itt

@@ -1,4 +1,4 @@
-{- let
+{- {- 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
@@ -10,10 +10,10 @@ in let
 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
+in let
   transport : (A : I -> Type) (a : A i0) -> A i1
     = \A a -> comp A i0 (\i -> []) a
-in {- let
+in let
   Jay : (A : Type) (x : A)
         (P : (y : A) -> Path (\i -> A) x y -> Type)
         (d : P x (\i -> x))
@@ -49,4 +49,31 @@ in let
 in let
   IisContr : (i : I) * ((j : I) -> Path (\i -> I) i j)
     = (i0, contrI)
-in IisContr
+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