From eb83b77bf3b6b1d11b0dbf08a408d55536338c3e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Am=C3=A9lia=20Liao?= <me@amelia.how>
Date: Sat, 27 Feb 2021 04:17:15 -0300
Subject: [PATCH] Implement cubical subtypes and composition

---
 intro.tt                   | 296 +++++++++++++++++++++++++++++++++++++
 src/Elab.hs                |  66 +++++----
 src/Elab/Eval.hs           | 115 +++++++++-----
 src/Elab/Eval/Formula.hs   |  10 +-
 src/Elab/Monad.hs          |  18 +--
 src/Elab/WiredIn.hs        |  86 ++++++++++-
 src/Elab/WiredIn.hs-boot   |   9 +-
 src/Presyntax/Lexer.x      |   9 +-
 src/Presyntax/Parser.y     |  35 +++--
 src/Presyntax/Presyntax.hs |   9 +-
 src/Presyntax/Tokens.hs    |   7 +-
 src/Syntax.hs              |  77 ++++++----
 src/Syntax/Pretty.hs       |  39 +++--
 test.tt                    |  90 -----------
 14 files changed, 643 insertions(+), 223 deletions(-)
 create mode 100644 intro.tt
 delete mode 100644 test.tt

diff --git a/intro.tt b/intro.tt
new file mode 100644
index 0000000..aa896d3
--- /dev/null
+++ b/intro.tt
@@ -0,0 +1,296 @@
+-- We begin by adding some primitive bindings using the PRIMITIVE pragma.
+-- 
+-- It goes like this: PRIMITIVE primName varName.
+-- 
+-- If the varName is dropped, then it's taken to be the same as primName.
+-- 
+-- If there is a previous declaration for the varName, then the type
+-- is checked against the internally-known "proper" type for the primitive.
+
+-- Universe of fibrant types
+{-# PRIMITIVE Type #-}
+
+-- Universe of non-fibrant types
+{-# PRIMITIVE Pretype #-}
+
+-- Fibrant is a fancy word for "has a composition structure". Most types
+-- we inherit from MLTT are fibrant:
+-- 
+-- Stuff like products Π, sums Σ, naturals, booleans, lists, etc., all
+-- have composition structures.
+-- 
+-- The non-fibrant types are part of the structure of cubical
+-- categories: The interval, partial elements, cubical subtypes, ...
+
+-- The interval
+---------------
+
+-- The interval has two endpoints i0 and i1.
+-- These form a de Morgan algebra.
+I : Pretype
+{-# PRIMITIVE Interval I #-}
+
+i0, i1 : I
+{-# PRIMITIVE i0 #-}
+{-# PRIMITIVE i1 #-}
+
+-- "minimum" on the interval
+iand : I -> I -> I
+{-# PRIMITIVE iand #-}
+
+-- "maximum" on the interval.
+ior : I -> I -> I
+{-# PRIMITIVE ior #-}
+
+-- The interpretation of iand as min and ior as max justifies the fact that
+-- ior i (inot i) != i1, since that equality only holds for the endpoints.
+
+-- inot i = 1 - i is a de Morgan involution.
+inot : I -> I
+{-# PRIMITIVE inot #-}
+
+-- Paths
+--------
+
+-- Since every function in type theory is internally continuous,
+-- and the two endpoints i0 and i1 are equal, we can take the type of
+-- equalities to be continuous functions out of the interval.
+-- That is, x ≡ y iff. ∃ f : I -> A, f i0 = x, f i1 = y.
+
+-- The type PathP generalises this to dependent products (i : I) -> A i.
+
+PathP : (A : I -> Pretype) -> A i0 -> A i1 -> Type
+{-# PRIMITIVE PathP #-}
+
+-- By taking the first argument to be constant we get the equality type
+-- Path.
+
+Path : {A : Pretype} -> A -> A -> Type
+Path {A} = PathP (\i -> A)
+
+-- reflexivity is given by constant paths
+
+refl : {A : Pretype} {x : A} -> Path x x
+refl {A} {x} i = x
+
+-- Symmetry (for dpeendent paths) is given by inverting the argument to the path, such that
+--   sym p i0 = p (inot i0) = p i1
+--   sym p i1 = p (inot i1) = p i0
+-- This has the correct endpoints.
+
+sym : {A : I -> Pretype} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x
+sym p i = p (inot i)
+
+id : {A : Type} -> A -> A
+id x = x
+
+the : (A : Pretype) -> A -> A
+the A x = x
+
+-- The eliminator for the interval says that if you have x : A i0 and y : A i1,
+-- and x ≡ y, then you can get a proof A i for every element of the interval.
+iElim : {A : I -> Pretype} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i
+iElim p i = p i
+
+-- This corresponds to the elimination principle for the HIT
+--   data I : Pretype where
+--     i0 i1 : I
+--     seg   : i0 ≡ i1
+
+-- The singleton subtype of A at x is the type of elements of y which
+-- are equal to x.
+Singl : (A : Type) -> A -> Type
+Singl A x = (y : A) * Path x y
+
+-- Contractible types are those for which there exists an element to which
+-- all others are equal.
+isContr : Type -> Type
+isContr A = (x : A) * ((y : A) -> Path x y)
+
+-- Using the connection \i j -> y.2 (iand i j), we can prove that
+-- singletons are contracible. Together with transport later on,
+-- we get the J elimination principle of paths.
+singContr : {A : Type} {a : A} -> isContr (Singl A a)
+singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))
+
+-- Some more operations on paths. By rearranging parentheses we get a
+-- proof that the images of equal elements are themselves equal.
+cong : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)
+cong f p i = f (p i)
+
+-- These satisfy definitional equalities, like congComp and congId, which are
+-- propositional in vanilla MLTT.
+congComp : {A : Type} {B : Type} {C : Type}
+           {f : A -> B} {g : B -> C} {x : A} {y : A}
+           (p : Path x y)
+        -> Path (cong g (cong f p)) (cong (\x -> g (f x)) p)
+congComp p = refl
+
+congId : {A : Type} {x : A} {y : A}
+         (p : Path x y)
+     -> Path (cong (id {A}) p) p
+congId p = refl
+
+-- Just like rearranging parentheses gives us cong, swapping the value
+-- and interval binders gives us function extensionality.
+funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
+         (h : (x : A) -> Path (f x) (g x))
+      -> Path f g
+funext h i x = h x i
+
+-- The proposition associated with an element of the interval
+-------------------------------------------------------------
+
+-- Associated with every element i : I of the interval, we have the type
+-- IsOne i which is inhabited only when i = i1. In the model, this
+-- corresponds to the map [φ] from the interval cubical set to the
+-- subobject classifier.
+
+IsOne : I -> Pretype
+{-# PRIMITIVE IsOne #-}
+
+-- The value itIs1 witnesses the fact that i1 = i1.
+itIs1 : IsOne i1
+
+-- Furthermore, if either of i or j are one, then so is (i or j).
+isOneL : {i : I} {j : I} -> IsOne i -> IsOne (ior i j)
+isOneR : {i : I} {j : I} -> IsOne j -> IsOne (ior i j)
+
+{-# PRIMITIVE itIs1 #-}
+{-# PRIMITIVE isOneL #-}
+{-# PRIMITIVE isOneR #-}
+
+-- Partial elements
+-------------------
+--
+-- Since a function I -> A has two endpoints, and a function I -> I -> A
+-- has four endpoints + four functions I -> A as "sides" (obtained by
+-- varying argument while holding the other as a bound variable), we
+-- refer to elements of I^n -> A as "cubes".
+
+-- This justifies the existence of partial elements, which are, as the
+-- name implies, partial cubes. Namely, a Partial φ A is an element of A
+-- which depends on a proof that IsOne φ.
+
+Partial : I -> Type -> Pretype
+{-# PRIMITIVE Partial #-}
+
+-- There is also a dependent version where the type A is itself a
+-- partial element.
+
+PartialP : (phi : I) -> Partial phi Type -> Pretype
+{-# PRIMITIVE PartialP #-}
+
+-- Why is Partial φ A not just defined as φ -> A? The difference is that
+-- Partial φ A has an internal representation which definitionally relates
+-- any two partial elements which "agree everywhere", that is, have
+-- equivalent values for every possible assignment of variables which
+-- makes IsOne φ hold.
+
+-- Cubical Subtypes
+--------------------
+
+-- Given A : Type, phi : I, and a partial element u : A defined on φ,
+-- we have the type Sub A phi u, notated A[phi -> u] in the output of
+-- the type checker, whose elements are "extensions" of u.
+
+-- That is, element of A[phi -> u] is an element of A defined everywhere
+-- (a total element), which, when IsOne φ, agrees with u.
+
+Sub  : (A : Type) (phi : I) -> Partial phi A -> Pretype
+{-# PRIMITIVE Sub #-}
+
+-- Every total element u : A can be made partial on φ by ignoring the
+-- constraint. Furthermore, this "totally partial" element agrees with
+-- the original total element on φ.
+inS : {A : Type} {phi : I} (u : A) -> Sub A phi (\x -> u)
+{-# PRIMITIVE inS #-}
+
+-- When IsOne φ, outS {A} {φ} {u} x reduces to u itIs1.
+-- This implements the fact that x agrees with u on φ.
+outS : {A : Type} {phi : I} {u : Partial phi A} -> Sub A phi u -> A
+{-# PRIMITIVE outS #-}
+
+-- The composition operation
+----------------------------
+
+-- Now that we have syntax for specifying partial cubes,
+-- and specifying that an element agrees with a partial cube,
+-- we can describe the composition operation.
+
+comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1
+{-# PRIMITIVE comp #-}
+
+-- In particular, when φ is a disjunction of the form
+-- (j = 0) || (j = 1), we can draw u as being a pair of lines forming a
+-- "tube", an open square with no floor or roof:
+--
+-- Given u = \j [ (i = i0) -> x, (i = i1) -> q j] on the extent i || ~i,
+-- we draw:
+--
+--          x         q i1
+--          |          |
+-- \j -> x  |          | \j -> q j
+--          |          |
+--          x         q i0
+--
+-- The composition operation says that, as long as we can provide a
+-- "floor" connecting x -- q i0, as a total element of A which, on
+-- phi, extends u i0, then we get the "roof" connecting x and q i1
+-- for free.
+--
+-- If we have a path p : x ≡ y, and q : y ≡ z, then we do get the
+-- "floor", and composition gets us the dotted line:
+-- 
+--        x..........z
+--        |          |
+--     x  |          | q j
+--        |          |
+--        x----------y
+--             p i
+
+trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z
+trans {A} {x} p q i =
+    comp (\i -> A)
+         {ior i (inot i)}
+         (\j [ (i = i0) -> x, (i = i1) -> q j ])
+         (inS (p i))
+
+-- In particular when the formula φ = i0 we get the "opposite face" to a
+-- single point, which corresponds to transport.
+
+transp : (A : I -> Type) (x : A i0) -> A i1
+transp A x = comp A (\i [ ]) (inS x)
+
+-- Since we have the iand operator, we can also derive the *filler* of a cube,
+-- which connects the given face and the output of composition.
+
+fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> (i : I) -> A i
+fill A {phi} u a0 i =
+    comp (\j -> A (iand i j))
+         (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])
+         (inS (outS a0))
+
+-- For instance, the filler of the previous composition square
+-- tells us that trans p refl = p:
+
+transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p
+transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)
+
+-- Reduction of composition
+---------------------------
+--
+-- Composition reduces on the structure of the family A : I -> Type to create
+-- the element a1 : (A i1)[phi -> u i1].
+--
+-- For instance, when filling a cube of functions, the behaviour is to
+-- first transport backwards along the domain, apply the function, then
+-- forwards along the codomain.
+
+transpFun : {A : Type} {B : Type} {C : Type} {D : Type} (p : Path A B) (q : Path C D)
+         -> (f : A -> C) -> Path (transp (\i -> p i -> q i) f)
+                                 (\x -> transp (\i -> q i) (f (transp (\i -> p (inot i)) x)))
+transpFun p q f = refl
+
+-- When considering the more general case of a composition respecing sides,
+-- the outer transport becomes a composition.
\ No newline at end of file
diff --git a/src/Elab.hs b/src/Elab.hs
index e0bf0e5..1210c26 100644
--- a/src/Elab.hs
+++ b/src/Elab.hs
@@ -11,7 +11,7 @@ import Data.Traversable
 import Data.Typeable
 import Data.Foldable
 
-import Elab.Eval.Formula (possible)
+import Elab.Eval.Formula (possible, truthAssignments)
 import Elab.WiredIn
 import Elab.Monad
 import Elab.Eval
@@ -52,20 +52,6 @@ infer (P.App p f x) = do
       x_nf <- eval x
       pure (App P.Ex (w f) x, a @@ x_nf)
 
-infer (P.Bracket ex) = do
-  nm <- getNameFor (T.pack "IsOne")
-  ty <- getNfType nm
-  porp <- isPiType P.Ex ty
-  case porp of
-    It'sProd d r w -> do
-      t <- check ex d
-      t_nf <- eval t
-      pure (App P.Ex (w (Ref nm)) t, r t_nf)
-    _ -> do
-      d <- newMeta VType
-      r <- newMeta VType
-      throwElab $ NotEqual ty (VPi P.Ex d (Closure (T.pack "x") (const r)))
-
 infer (P.Proj1 x) = do
   (tm, ty) <- infer x
   (d, _, wp) <- isSigmaType ty
@@ -112,7 +98,7 @@ check (P.Lam p v b) ty = do
       unify (tm_nf @@ VI1) ri
         `catchElab` (throwElab . WhenCheckingEndpoint le ri VI1)
 
-      pure (wp (PathIntro (quote (fun li)) tm))
+      pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
 
     It'sPartial phi a wp ->
       assume (Bound v) (VIsOne phi) $
@@ -147,17 +133,40 @@ check (P.Sigma s d r) ty = do
 
 check (P.LamSystem bs) ty = do
   (extent, dom) <- isPartialType ty
+  let dom_q = quote dom
   eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
-    formula <- checkFormula formula
-    rhs <- check rhs dom
-    pure (n, (formula, rhs))
+    phi <- checkFormula (P.condF formula)
+    rhses <-
+        case P.condV formula of
+          Just t -> assume (Bound t) (VIsOne phi) $ do
+            env <- ask
+            for (truthAssignments phi (getEnv env)) $ \e -> do
+              let env' = env{ getEnv = e }
+              check rhs (eval' env' dom_q)
+          Nothing -> do
+            env <- ask
+            for (truthAssignments phi (getEnv env)) $ \e -> do
+              let env' = env{ getEnv = e }
+              check rhs (eval' env' dom_q)
+    pure (n, (phi, (P.condV formula, head rhses)))
 
   unify extent (foldl ior VI0 (map (fst . snd) eqns))
 
-  for_ eqns $ \(n, (formula, rhs)) ->
-    for_ eqns $ \(n', (formula', rhs')) -> do
-      let truth = possible mempty (iand formula formula')
-      when ((n /= n') && fst truth) $ do
+  for_ eqns $ \(n, (formula, (binding, rhs))) -> do
+    let
+      k = case binding of
+        Just v -> assume (Bound v) (VIsOne formula)
+        Nothing -> id
+    k $ for_ eqns $ \(n', (formula', (binding, rhs'))) -> do
+      let
+        k = case binding of
+          Just v -> assume (Bound v) (VIsOne formula)
+          Nothing -> id
+        truth = possible mempty (iand formula formula')
+        add [] = id
+        add ((~(HVar x), True):xs) = define x VI VI1 . add xs
+        add ((~(HVar x), False):xs) = define x VI VI0 . add xs
+      k $ when ((n /= n') && fst truth) . add (Map.toList (snd truth)) $ do
         vl <- eval rhs
         vl' <- eval rhs'
         unify vl vl'
@@ -168,7 +177,10 @@ check (P.LamSystem bs) ty = do
           `withNote` (pretty "Consider this face, where both are true:" <+> showFace (snd truth))
 
   name <- newName
-  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, y)) eqns))))
+  let
+    mkB name (Just v, b) = App P.Ex (Lam P.Ex v b) (Ref name)
+    mkB _ (Nothing, b) = b
+  pure (Lam P.Ex name (System (Map.fromList (map (\(_, (x, y)) -> (quote x, mkB (Bound name) y)) eqns))))
 
 check exp ty = do
   (tm, has) <- switch $ infer exp
@@ -195,7 +207,7 @@ isSort :: NFType -> ElabM ()
 isSort VType                = pure ()
 isSort VTypeω               = pure ()
 isSort vt@(VNe HMeta{} _)   = unify vt VType
-isSort vt = liftIO . throwIO $ NotEqual vt VType
+isSort vt = throwElab $ NotEqual vt VType
 
 data ProdOrPath
   = It'sProd { prodDmn  :: NFType
@@ -275,7 +287,7 @@ checkStatement (P.Defn name rhs) k = do
     Just (ty_nf, nm) -> do
       case nm of
         VVar (Defined n') | n' == name -> pure ()
-        _ -> liftIO . throwIO $ Redefinition (Defined name)
+        _ -> throwElab $ Redefinition (Defined name)
 
       rhs <- check rhs ty_nf
       rhs_nf <- eval rhs
@@ -285,7 +297,7 @@ checkStatement (P.Builtin winame var) k = do
   wi <-
     case Map.lookup winame wiredInNames of
       Just wi -> pure wi
-      _ -> liftIO . throwIO $ NoSuchPrimitive winame
+      _ -> throwElab $ NoSuchPrimitive winame
 
   let
     check = do
diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs
index 5422e19..dbe50fe 100644
--- a/src/Elab/Eval.hs
+++ b/src/Elab/Eval.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE DeriveAnyClass #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
 module Elab.Eval where
 
 import Control.Monad.Reader
@@ -31,21 +32,24 @@ import Syntax
 import System.IO.Unsafe
 
 import {-# SOURCE #-} Elab.WiredIn
+import GHC.Stack
 
 eval :: Term -> ElabM Value
 eval t = asks (flip eval' t)
 
 forceIO :: MonadIO m => Value -> m Value
-forceIO vl@(VNe (HMeta (MV _ cell)) args) = do
+forceIO mv@(VNe (HMeta (MV id cell)) args) = do
   solved <- liftIO $ readIORef cell
   case solved of
     Just vl -> forceIO $ foldl applProj vl args
-    Nothing -> pure vl
+    Nothing -> pure mv
+forceIO (VComp line phi u a0) = comp line <$> forceIO phi <*> pure u <*> pure a0
 forceIO x = pure x
 
 applProj :: Value -> Projection -> Value
 applProj fun (PApp p arg)     = vApp p fun arg
 applProj fun (PIElim l x y i) = ielim l x y fun i
+applProj fun (POuc a phi u)   = outS a phi u fun
 applProj fun PProj1           = vProj1 fun
 applProj fun PProj2           = vProj2 fun
 
@@ -66,6 +70,7 @@ zonkIO (VNe hd sp) = do
   where
     zonkSp (PApp p x) = PApp p <$> zonkIO x
     zonkSp (PIElim l x y i) = PIElim <$> zonkIO l <*> zonkIO x <*> zonkIO y <*> zonkIO i
+    zonkSp (POuc a phi u) = POuc <$> zonkIO a <*> zonkIO phi <*> zonkIO u
     zonkSp PProj1 = pure PProj1
     zonkSp PProj2 = pure PProj2
 zonkIO (VLam p (Closure s k)) = pure $ VLam p (Closure s (zonk . k))
@@ -74,7 +79,7 @@ zonkIO (VSigma d (Closure s k)) = VSigma <$> zonkIO d <*> pure (Closure s (zonk
 zonkIO (VPair a b) = VPair <$> zonkIO a <*> zonkIO b
 
 zonkIO (VPath line x y) = VPath <$> zonkIO line <*> zonkIO x <*> zonkIO y
-zonkIO (VLine line f) = VLine <$> zonkIO line <*> zonkIO f
+zonkIO (VLine line x y f) = VLine <$> zonkIO line <*> zonkIO x <*> zonkIO y <*> zonkIO f
 
 -- Sorts
 zonkIO VType = pure VType
@@ -95,15 +100,18 @@ zonkIO VItIsOne = pure VItIsOne
 
 zonkIO (VPartial x y)  = VPartial <$> zonkIO x <*> zonkIO y
 zonkIO (VPartialP x y) = VPartialP <$> zonkIO x <*> zonkIO y
-zonkIO (VSystem fs) =
-  do
-    t <- for (Map.toList fs) $ \(a, b) -> (,) <$> zonkIO a <*> zonkIO b
-    pure (mkVSystem (Map.fromList t))
-  where
-    mkVSystem map =
-      case Map.lookup VI1 map of
-        Just x -> x
-        Nothing -> VSystem map
+zonkIO (VSystem fs) = do
+  t <- for (Map.toList fs) $ \(a, b) -> (,) <$> zonkIO a <*> zonkIO b
+  pure (mkVSystem (Map.fromList t))
+zonkIO (VSub a b c) = VSub <$> zonkIO a <*> zonkIO b <*> zonkIO c
+zonkIO (VInc a b c) = VInc <$> zonkIO a <*> zonkIO b <*> zonkIO c
+zonkIO (VComp a b c d) = comp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d
+
+mkVSystem :: Map.Map Value Value -> Value
+mkVSystem map =
+  case Map.lookup VI1 map of
+    Just x -> x
+    Nothing -> VSystem (Map.filterWithKey (\k _ -> k /= VI0) map)
 
 zonk :: Value -> Value
 zonk = unsafePerformIO . zonkIO
@@ -112,7 +120,7 @@ eval' :: ElabEnv -> Term -> Value
 eval' env (Ref x) =
   case Map.lookup x (getEnv env) of
     Just (_, vl) -> vl
-    _ -> error "variable not in scope when evaluating"
+    _ -> VVar x
 eval' env (App p f x) = vApp p (eval' env f) (eval' env x)
 
 eval' env (Lam p s t) =
@@ -146,7 +154,7 @@ eval' e (INot x) = inot (eval' e x)
 
 eval' e (PathP l a b) = VPath (eval' e l) (eval' e a) (eval' e b)
 eval' e (IElim l x y f i) = ielim (eval' e l) (eval' e x) (eval' e y) (eval' e f) (eval' e i)
-eval' e (PathIntro p f) = VLine (eval' e p) (eval' e f)
+eval' e (PathIntro p x y f) = VLine (eval' e p) (eval' e x) (eval' e y) (eval' e f)
 
 eval' e (IsOne i)  = VIsOne (eval' e i)
 eval' e (IsOne1 i) = VIsOne1 (eval' e i)
@@ -157,31 +165,40 @@ eval' e (Partial x y)  = VPartial (eval' e x) (eval' e y)
 eval' e (PartialP x y) = VPartialP (eval' e x) (eval' e y)
 eval' e (System fs) = VSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
 
-vApp :: Plicity -> Value -> Value -> Value
+eval' e (Sub a phi u)   = VSub (eval' e a) (eval' e phi) (eval' e u)
+eval' e (Inc a phi u)   = VInc (eval' e a) (eval' e phi) (eval' e u)
+eval' e (Ouc a phi u x) = outS (eval' e a) (eval' e phi) (eval' e u) (eval' e x)
+
+eval' e (Comp a phi u a0) = comp (eval' e a) (eval' e phi) (eval' e u) (eval' e a0)
+
+vApp :: HasCallStack => Plicity -> Value -> Value -> Value
 vApp p (VLam p' k) arg
   | p == p'   = clCont k arg
   | otherwise = error $ "wrong plicity " ++ show p ++ " vs " ++ show p' ++ " in app " ++ show (App p (quote (VLam p' k)) (quote arg))
 vApp p (VNe h sp) arg  = VNe h (sp Seq.:|> PApp p arg)
+vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs)
 vApp _ x _             = error $ "can't apply " ++ show x
 
-(@@) :: Value -> Value -> Value
+(@@) :: HasCallStack => Value -> Value -> Value
 (@@) = vApp Ex
 infixl 9 @@
 
 vProj1 :: Value -> Value
 vProj1 (VPair a _) = a
 vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1)
+vProj1 (VSystem fs) = VSystem (fmap vProj1 fs)
 vProj1 x = error $ "can't proj1 " ++ show x
 
 vProj2 :: Value -> Value
 vProj2 (VPair _ b) = b
 vProj2 (VNe h sp)  = VNe h (sp Seq.:|> PProj2)
+vProj2 (VSystem fs) = VSystem (fmap vProj2 fs)
 vProj2 x = error $ "can't proj2 " ++ show x
 
 data NotEqual = NotEqual Value Value
   deriving (Show, Typeable, Exception)
 
-unify' :: Value -> Value -> ElabM ()
+unify' :: HasCallStack => Value -> Value -> ElabM ()
 unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs
   go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs
@@ -189,18 +206,23 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VNe x a) (VNe x' a')
     | x == x', length a == length a' =
       traverse_ (uncurry unify'Spine) (Seq.zip a a')
+    | x == HVar (Bound (T.pack "y")), x' == HVar (Bound (T.pack "A")) = error "what"
 
-  go (VNe _hd (_ Seq.:|> PIElim _l x y i)) rhs =
+  go lhs@(VNe _hd (_ Seq.:|> PIElim _l x y i)) rhs =
     case force i of
       VI0 -> unify' x rhs
       VI1 -> unify' y rhs
-      _   -> fail
+      _   -> case rhs of
+        VSystem sys -> goSystem (flip unify') sys lhs
+        _ -> fail
 
-  go rhs (VNe _hd (_ Seq.:|> PIElim _l x y i)) =
+  go lhs rhs@(VNe _hd (_ Seq.:|> PIElim _l x y i)) =
     case force i of
-      VI0 -> unify' rhs x
-      VI1 -> unify' rhs y
-      _   -> fail
+      VI0 -> unify' lhs x
+      VI1 -> unify' lhs y
+      _   -> case lhs of
+        VSystem sys -> goSystem unify' sys rhs
+        _ -> fail
 
   go (VLam p (Closure _ k)) vl = do
     t <- VVar . Bound <$> newName
@@ -233,13 +255,13 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     unify' x x'
     unify' y y'
 
-  go (VLine l p) p' = do
+  go (VLine l x y p) p' = do
     n <- VVar . Bound <$> newName
-    unify (p @@ n) (ielim l (l @@ VI0) (l @@ VI1) p' n)
+    unify (p @@ n) (ielim l x y p' n)
 
-  go p' (VLine l p) = do
+  go p' (VLine l x y p) = do
     n <- VVar . Bound <$> newName
-    unify (ielim l (l @@ VI0) (l @@ VI1) p' n) (p @@ n)
+    unify (ielim l x y p' n) (p @@ n)
 
   go (VIsOne x) (VIsOne y) = unify' x y
 
@@ -254,12 +276,30 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   go (VPartial phi r) (VPartial phi' r')   = unify' phi phi' *> unify r r'
   go (VPartialP phi r) (VPartialP phi' r') = unify' phi phi' *> unify r r'
 
+  go (VSub a phi u) (VSub a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
+  go (VInc a phi u) (VInc a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
+
+  go (VComp a phi u a0) (VComp a' phi' u' a0') =
+    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
+
+  go (VSystem sys) rhs = goSystem unify' sys rhs
+  go rhs (VSystem sys) = goSystem (flip unify') sys rhs
+
   go x y =
     case (toDnf x, toDnf y) of
       (Just xs, Just ys) -> unify'Formula xs ys
       _ -> fail
 
-  fail = liftIO . throwIO $ NotEqual topa topb
+  goSystem :: (Value -> Value -> ElabM ()) -> Map.Map Value Value -> Value -> ElabM ()
+  goSystem k sys rhs = do
+    let rhs_q = quote rhs
+    env <- ask
+    for_ (Map.toList sys) $ \(f, i) -> do
+      let i_q = quote i
+      for (truthAssignments f (getEnv env)) $ \e ->
+        k (eval' env{getEnv = e} i_q) (eval' env{getEnv = e} rhs_q)
+
+  fail = throwElab $ NotEqual topa topb
 
   unify'Spine (PApp a v) (PApp a' v')
     | a == a' = unify' v v'
@@ -268,6 +308,8 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
   unify'Spine PProj2 PProj2 = pure ()
 
   unify'Spine (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' i j
+  unify'Spine (POuc a phi u) (POuc a' phi' u') =
+    traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
 
   unify'Spine _ _ = fail
 
@@ -275,7 +317,7 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
     | compareDNFs x y = pure ()
     | otherwise = fail
 
-unify :: Value -> Value -> ElabM ()
+unify :: HasCallStack => Value -> Value -> ElabM ()
 unify a b = unify' a b `catchElab` \(_ :: NotEqual) -> liftIO $ throwIO (NotEqual a b)
 
 isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
@@ -338,7 +380,7 @@ checkScope scope (VNe h sp) =
   do
     case h of
       HVar v@Bound{} ->
-        unless (v `Set.member` scope) . liftIO . throwIO $
+        unless (v `Set.member` scope) . throwElab $
           NotInScope v
       HVar{} -> pure ()
       HMeta{} -> pure ()
@@ -346,6 +388,7 @@ checkScope scope (VNe h sp) =
   where
     checkProj (PApp _ t) = checkScope scope t
     checkProj (PIElim l x y i) = traverse_ (checkScope scope) [l, x, y, i]
+    checkProj (POuc a phi u) = traverse_ (checkScope scope) [a, phi, u]
     checkProj PProj1 = pure ()
     checkProj PProj2 = pure ()
 
@@ -374,7 +417,7 @@ checkScope s (VIOr x y)  = traverse_ (checkScope s) [x, y]
 checkScope s (VINot x)   = checkScope s x
 
 checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
-checkScope s (VLine _ line)   = checkScope s line
+checkScope s (VLine _ _ _ line)   = checkScope s line
 
 checkScope s (VIsOne x) = checkScope s x
 checkScope s (VIsOne1 x) = checkScope s x
@@ -386,15 +429,19 @@ checkScope s (VPartialP x y) = traverse_ (checkScope s) [x, y]
 checkScope s (VSystem fs) =
   for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope s) [x, y]
 
+checkScope s (VSub a b c) = traverse_ (checkScope s) [a, b, c]
+checkScope s (VInc a b c) = traverse_ (checkScope s) [a, b, c]
+checkScope s (VComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0]
+
 checkSpine :: Set Name -> Seq Projection -> ElabM [T.Text]
 checkSpine scope (PApp Ex (VVar n@(Bound t)) Seq.:<| xs)
-  | n `Set.member` scope = liftIO . throwIO $ NonLinearSpine n
+  | n `Set.member` scope = throwElab $ NonLinearSpine n
   | otherwise = (t:) <$> checkSpine scope xs
-checkSpine _     (p Seq.:<| _) = liftIO . throwIO $ SpineProj p
+checkSpine _     (p Seq.:<| _) = throwElab $ SpineProj p
 checkSpine _     Seq.Empty = pure []
 
 newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
   deriving (Show, Typeable, Exception)
 
 newtype SpineProjection = SpineProj { getSpineProjection :: Projection }
-  deriving (Show, Typeable, Exception)
+  deriving (Show, Typeable, Exception)
\ No newline at end of file
diff --git a/src/Elab/Eval/Formula.hs b/src/Elab/Eval/Formula.hs
index cfa6ccf..274f422 100644
--- a/src/Elab/Eval/Formula.hs
+++ b/src/Elab/Eval/Formula.hs
@@ -7,7 +7,6 @@ import Data.Map.Strict (Map)
 import Syntax
 
 import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
-import Debug.Trace (traceShow)
 
 toDnf :: Value -> Maybe Value
 toDnf (VNe _ _) = Nothing
@@ -56,6 +55,15 @@ possible sc VI0 = (False, sc)
 possible sc VI1 = (True, sc)
 possible sc _ = (False, sc)
 
+truthAssignments :: NFEndp -> Map Name (NFType, NFEndp) -> [Map Name (NFType, NFEndp)]
+truthAssignments VI0 m = []
+truthAssignments VI1 m = pure m
+truthAssignments (VIOr x y) m = truthAssignments x m ++ truthAssignments y m
+truthAssignments (VIAnd x y) m = truthAssignments x =<< truthAssignments y m
+truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) m)
+truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) m)
+truthAssignments x _ = error $ "impossible formula: " ++ show x
+
 idist :: Value -> Value -> Value
 idist (VIOr x y) z = (x `idist` z) `ior` (y `idist` z)
 idist z (VIOr x y) = (z `idist` x) `ior` (z `idist` y)
diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs
index 39309f7..438f19a 100644
--- a/src/Elab/Monad.hs
+++ b/src/Elab/Monad.hs
@@ -14,9 +14,11 @@ import Data.Map.Strict (Map)
 import Data.Text (Text)
 import Data.Typeable
 
-import Syntax
 import qualified Presyntax.Presyntax as P
 
+import Syntax.Pretty (getNameText)
+import Syntax
+
 data ElabEnv =
   ElabEnv { getEnv      :: Map Name (NFType, Value)
 
@@ -49,10 +51,6 @@ assumes nm ty = local go where
            , whereBound = maybe (whereBound x) (\l -> Map.union (Map.fromList (zip nm (repeat l))) (whereBound x)) (currentSpan x)
            }
 
-getNameText :: Name -> Text
-getNameText (Bound x) = x
-getNameText (Defined x) = x
-
 define :: Name -> Value -> Value -> ElabM a -> ElabM a
 define nm ty vl = local go where
   go x = x { getEnv = Map.insert nm (ty, vl) (getEnv x), nameMap = Map.insert (getNameText nm) nm (nameMap x) }
@@ -62,14 +60,14 @@ getValue nm = do
   vl <- asks (Map.lookup nm . getEnv)
   case vl of
     Just v -> pure (snd v)
-    Nothing -> liftIO . throwIO $ NotInScope nm
+    Nothing -> throwElab $ NotInScope nm
 
 getNfType :: Name -> ElabM NFType
 getNfType nm = do
   vl <- asks (Map.lookup nm . getEnv)
   case vl of
     Just v -> pure (fst v)
-    Nothing -> liftIO . throwIO $ NotInScope nm
+    Nothing -> throwElab $ NotInScope nm
 
 getNameFor :: Text -> ElabM Name
 getNameFor x = do
@@ -82,7 +80,7 @@ switch :: ElabM a -> ElabM a
 switch k =
   do
     depth <- asks pingPong
-    when (depth >= 128) $ liftIO $ throwIO StackOverflow
+    when (depth >= 128) $ throwElab StackOverflow
     local go k
   where go e = e { pingPong = pingPong e + 1 }
 
@@ -134,6 +132,6 @@ tryElab :: Exception e => ElabM a -> ElabM (Either e a)
 tryElab k = do
   env <- ask
   liftIO $ (Right <$> runElab k env) `catch` \e -> pure (Left e)
-  
+
 throwElab :: Exception e => e -> ElabM a
-throwElab = liftIO . throwIO
\ No newline at end of file
+throwElab = liftIO . throwIO
diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs
index 53a6c37..36ed945 100644
--- a/src/Elab/WiredIn.hs
+++ b/src/Elab/WiredIn.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE ViewPatterns #-}
 module Elab.WiredIn where
 
 import Syntax
@@ -14,6 +15,7 @@ import Data.Typeable
 import qualified Presyntax.Presyntax as P
 import Elab.Eval
 import qualified Data.Sequence as Seq
+import qualified Data.Text as T
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType
@@ -28,7 +30,7 @@ wiType WiIOr      = VI ~> VI ~> VI
 wiType WiINot     = VI ~> VI
 wiType WiPathP    = dprod (VI ~> VTypeω) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
 
-wiType WiIsOne    = VI ~> VType
+wiType WiIsOne    = VI ~> VTypeω
 wiType WiItIsOne  = VIsOne VI1
 wiType WiIsOne1   = forAll VI \i -> forAll VI \j -> VIsOne i ~> VIsOne (ior i j)
 wiType WiIsOne2   = forAll VI \i -> forAll VI \j -> VIsOne j ~> VIsOne (ior i j)
@@ -36,6 +38,12 @@ wiType WiIsOne2   = forAll VI \i -> forAll VI \j -> VIsOne j ~> VIsOne (ior i j)
 wiType WiPartial  = VI ~> VType ~> VTypeω
 wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω
 
+wiType WiSub      = dprod VType \a -> dprod VI \phi -> VPartial phi a ~> VTypeω
+wiType WiInS      = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (VLam P.Ex (Closure "x" (const u)))
+wiType WiOutS     = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a) \u -> VSub a phi u ~> a
+
+wiType WiComp     = dprod (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
+
 wiValue :: WiredIn -> Value
 wiValue WiType     = VType
 wiValue WiPretype  = VTypeω
@@ -56,6 +64,11 @@ wiValue WiIsOne2  = forallI \_ -> forallI \_ -> fun VIsOne2
 
 wiValue WiPartial  = fun \phi -> fun \r -> VPartial phi r
 wiValue WiPartialP = fun \phi -> fun \r -> VPartialP phi r
+wiValue WiSub      = fun \a -> fun \phi -> fun \u -> VSub a phi u
+wiValue WiInS      = forallI \a -> forallI \phi -> fun \u -> VInc a phi u
+wiValue WiOutS     = forallI \a -> forallI \phi -> forallI \u -> fun \x -> outS a phi u x
+-- wiValue WiComp     = forAll (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
+wiValue WiComp     = fun \a -> forallI \phi -> fun \u -> fun \x -> comp a phi u x
 
 (~>) :: Value -> Value -> Value
 a ~> b = VPi P.Ex a (Closure "_" (const b))
@@ -92,6 +105,11 @@ wiredInNames = Map.fromList
 
   , ("Partial", WiPartial)
   , ("PartialP", WiPartialP)
+  , ("Sub", WiSub)
+  , ("inS", WiInS)
+  , ("outS", WiOutS)
+
+  , ("comp", WiComp)
   ]
 
 newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
@@ -137,6 +155,68 @@ inot = \case
 ielim :: Value -> Value -> Value -> Value -> NFEndp -> Value
 ielim _line _left _right fn i =
   case force fn of
-    VLine _ fun -> fun @@ i
+    VLine _ _ _ fun -> fun @@ i
     VNe n sp -> VNe n (sp Seq.:|> PIElim _line _left _right i)
-    _ -> error $ "can't ielim " ++ show fn
\ No newline at end of file
+    _ -> error $ "can't ielim " ++ show fn
+
+outS :: NFSort -> NFEndp -> Value -> Value -> Value
+outS _ (force -> VI1) u _  = u @@ VItIsOne
+outS _ _phi _ (VInc _ _ x) = x 
+outS a phi u  (VNe x sp)   = VNe x (sp Seq.:|> POuc a phi u)
+outS _ _ _ v               = error $ "can't outS " ++ show v
+
+-- Composition
+comp :: NFLine -> NFEndp -> Value -> Value -> Value
+comp _ VI1 u _ = u @@ VI1 @@ VItIsOne
+comp a phi u (VInc _ _ a0) =
+  case a @@ VNe (HVar (Bound (T.pack "x"))) Seq.empty of
+    VPi{} -> 
+      let
+        plic i = let VPi p _ _ = a @@ i in p
+        dom  i = let VPi _ d _ = a @@ i in d
+        rng  i = let VPi _ _ (Closure _ r) = a @@ i in r
+
+        y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i
+        ybar i y = y' (inot i) y
+       in VLam (plic VI1) . Closure "x" $ \arg ->
+              comp (fun \i -> rng i (ybar i arg))
+                   phi
+                   (system \i isone -> vApp (plic i) (u @@ i @@ isone) (ybar i arg))
+                   (VInc (rng VI0 (ybar VI0 arg)) phi (vApp (plic VI0) a0 (ybar VI0 arg)))
+    VSigma{} ->
+      let
+        dom i = let VSigma d _ = a @@ i in d
+        rng i = let VSigma _ (Closure _ r) = a @@ i in r
+
+        w i = fill (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0)) i
+        c1 = comp (fun dom) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (dom VI0) phi (vProj1 a0))
+        c2 = comp (fun (($ w VI1) . rng)) phi (system \i isone -> vProj1 (u @@ i @@ isone)) (VInc (rng VI0 (dom VI0)) phi (vProj2 a0))
+       in
+         VPair c1 c2
+    VPath{} ->
+      let
+        a' i = let VPath a _ _ = a @@ i in a
+        u' i = let VPath _ u _ = a @@ i in u
+        v' i = let VPath _ _ v = a @@ i in v
+      in
+        VLine (a' VI1 @@ VI1) (u' VI1) (v' VI1) $ fun \j ->
+          comp (fun a')
+            (phi `ior` j `ior` inot j)
+            (system \i isone -> mkVSystem (Map.fromList [ (phi, ielim (a' VI0) (u' VI0) (v' VI0) (u @@ i @@ isone) j)
+                                                        , (j, v' i)
+                                                        , (inot j, u' i)]))
+            (VInc (a' VI0 @@ VI0 @@ j) phi (ielim (a' VI0 @@ VI0) (u' VI0) (v' VI0) a0 j))
+
+    _ -> VComp a phi u a0
+comp a phi u a0 = VComp a phi u a0
+
+system :: (Value -> Value -> Value) -> Value
+system k = fun \i -> fun \isone -> k i isone
+
+fill :: NFLine -> NFEndp -> Value -> Value -> NFEndp -> Value
+fill a phi u a0 j =
+  comp (fun \i -> a @@ (i `iand` j))
+       (phi `ior` inot j)
+       (fun \i -> fun \isone -> mkVSystem (Map.fromList [ (phi, u @@ (i `iand` j) @@ isone)
+                                                        , (inot j, a0)]))
+       a0
\ No newline at end of file
diff --git a/src/Elab/WiredIn.hs-boot b/src/Elab/WiredIn.hs-boot
index efa3482..20a5b57 100644
--- a/src/Elab/WiredIn.hs-boot
+++ b/src/Elab/WiredIn.hs-boot
@@ -5,6 +5,9 @@ import Syntax
 wiType  :: WiredIn -> NFType
 wiValue :: WiredIn -> NFType
 
-iand, ior :: Value -> Value -> Value
-inot :: Value -> Value
-ielim :: Value -> Value -> Value -> Value -> NFEndp -> Value
\ No newline at end of file
+iand, ior :: NFEndp -> NFEndp -> NFEndp
+inot      :: NFEndp -> NFEndp
+ielim     :: NFSort -> Value -> Value -> Value -> NFEndp -> Value
+
+outS :: NFSort -> NFEndp -> Value -> Value -> Value
+comp :: NFLine -> NFEndp -> Value -> Value -> Value
\ No newline at end of file
diff --git a/src/Presyntax/Lexer.x b/src/Presyntax/Lexer.x
index a93c588..71de049 100644
--- a/src/Presyntax/Lexer.x
+++ b/src/Presyntax/Lexer.x
@@ -3,6 +3,7 @@ module Presyntax.Lexer where
 
 import qualified Data.ByteString.Lazy as Lbs
 import qualified Data.Text.Encoding as T
+import qualified Data.Text as T
 
 import Presyntax.Tokens
 }
@@ -17,7 +18,7 @@ tokens :-
   $white_nol+                   ;
   "--" .* \n                    ;
   
-<0,prtext> $alpha [$alpha $digit \_ \']* { yield TokVar }
+<0,prtext> $alpha [$alpha $digit \_ \']* { yield tokVar }
 
 -- zero state: normal lexing
 <0> \=                            { always TokEqual }
@@ -117,4 +118,10 @@ offsideRule (AlexPn _ line col, _, s, _) _
         popStartCode
         alexMonadScan
       LT -> alexError "wrong ass indentation"
+
+tokVar :: T.Text -> TokenClass
+tokVar text =
+  case T.unpack text of
+    "as" -> TokAs
+    _ -> TokVar text
 }
\ No newline at end of file
diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y
index 2720a46..ed477fb 100644
--- a/src/Presyntax/Parser.y
+++ b/src/Presyntax/Parser.y
@@ -50,6 +50,7 @@ import Prelude hiding (span)
   '='         { Token TokEqual _ _ }
   ','         { Token TokComma _ _ }
   '*'         { Token TokStar _ _ }
+  'as'        { Token TokAs _ _ }
 
   '&&'        { Token TokAnd _ _ }
   '||'        { Token TokOr _ _ }
@@ -66,16 +67,16 @@ import Prelude hiding (span)
 
 Exp :: { Expr }
 Exp
-  : '\\' LambdaList '->' Exp          { span $1 $4 $ makeLams $2 $4 }
-  | '\\' '{' System '}'               { span $1 $4 $ LamSystem $3 }
-  | '(' var ':' Exp ')' ProdTail      { span $1 $6 $ Pi Ex (getVar $2) $4 $6 }
-  | '{' var ':' Exp '}' ProdTail      { span $1 $6 $ Pi Im (getVar $2) $4 $6 }
-  | ExpApp '->' Exp                   { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 }
+  : '\\' LambdaList '->' Exp             { span $1 $4 $ makeLams $2 $4 }
+  | '\\' MaybeLambdaList '[' System ']'  { span $1 $5 $ makeLams $2 $ LamSystem $4 }
+  | '(' var ':' Exp ')' ProdTail         { span $1 $6 $ Pi Ex (getVar $2) $4 $6 }
+  | '{' var ':' Exp '}' ProdTail         { span $1 $6 $ Pi Im (getVar $2) $4 $6 }
+  | ExpApp '->' Exp                      { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 }
 
-  | '(' var ':' Exp ')' '*'  Exp      { span $1 $7 $ Sigma (getVar $2) $4 $7 }
-  | ExpApp '*' Exp                    { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
+  | '(' var ':' Exp ')' '*'  Exp         { span $1 $7 $ Sigma (getVar $2) $4 $7 }
+  | ExpApp '*' Exp                       { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
 
-  | ExpApp                            { $1 }
+  | ExpApp                               { $1 }
 
 ExpApp :: { Expr }
   : ExpApp ExpProj         { span $1 $2 $ App Ex $1 $2 }
@@ -94,13 +95,16 @@ Tuple :: { Expr }
 Atom :: { Expr }
   : var           { span $1 $1 $ Var (getVar $1) }
   | '(' Tuple ')' { span $1 $3 $ $2 }
-  | '[' Exp ']'   { span $1 $3 $ Bracket $2 }
 
 ProdTail :: { Expr }
   : '(' VarList ':' Exp ')' ProdTail  { span $1 $6 $ makePis Ex (thd $2) $4 $6 }
   | '{' VarList ':' Exp '}' ProdTail  { span $1 $6 $ makePis Im (thd $2) $4 $6 }
   | '->' Exp                          { span $2 $2 $ $2 }
 
+MaybeLambdaList :: { [(Plicity, Text)] }
+  : {- empty -} { [] }
+  | LambdaList  { $1 }
+
 LambdaList :: { [(Plicity, Text)] }
   : var            { [(Ex, getVar $1)] }
   | var LambdaList { (Ex, getVar $1):$2 }
@@ -130,6 +134,7 @@ ReplStatement :: { Statement }
 
 Program :: { [Statement] }
   : Statement               { [$1] }
+  | Semis Program           { $2 }
   | Statement Semis Program { $1:$3 }
 
 Semis :: { () }
@@ -140,13 +145,17 @@ Pragma :: { Statement }
   : 'PRIMITIVE' var var { Builtin (getVar $2) (getVar $3) }
   | 'PRIMITIVE' var     { Builtin (getVar $2) (getVar $2) }
 
-System :: { [(Formula, Expr)] }
+System :: { [(Condition, Expr)] }
   : {- empty system -}            { [] }
   | NeSystem                      { $1 }
 
-NeSystem :: { [(Formula, Expr) ]}
-  : Formula '->' Exp              { [($1, $3)] }
-  | Formula '->' Exp ',' NeSystem { ($1, $3):$5 }
+NeSystem :: { [(Condition, Expr) ]}
+  : SystemLhs '->' Exp              { [($1, $3)] }
+  | SystemLhs '->' Exp ',' NeSystem { ($1, $3):$5 }
+
+SystemLhs :: { Condition }
+  : Formula 'as' var { Condition $1 (Just (getVar $3)) }
+  | Formula          { Condition $1 Nothing }
 
 Formula :: { Formula }
   : Disjn            { $1 }
diff --git a/src/Presyntax/Presyntax.hs b/src/Presyntax/Presyntax.hs
index b9292f1..581cef3 100644
--- a/src/Presyntax/Presyntax.hs
+++ b/src/Presyntax/Presyntax.hs
@@ -19,15 +19,16 @@ data Expr
   | Proj1 Expr
   | Proj2 Expr
 
-  -- application of IsOne primitive is written like [ φ ]
-  | Bracket Expr
-
   -- System
-  | LamSystem [(Formula, Expr)]
+  | LamSystem [(Condition, Expr)]
 
   | Span Expr Posn Posn
   deriving (Eq, Show, Ord)
 
+data Condition
+  = Condition { condF :: Formula, condV :: Maybe Text }
+  deriving (Eq, Show, Ord)
+
 data Formula
   = FIs1 Text
   | FIs0 Text
diff --git a/src/Presyntax/Tokens.hs b/src/Presyntax/Tokens.hs
index 2bf2086..07e6222 100644
--- a/src/Presyntax/Tokens.hs
+++ b/src/Presyntax/Tokens.hs
@@ -38,6 +38,8 @@ data TokenClass
   | TokAnd
   | TokOr
 
+  | TokAs
+
   | TokSemi
   deriving (Eq, Show, Ord)
 
@@ -63,8 +65,9 @@ tokSize TokArrow = 2
 tokSize TokPi1 = 2
 tokSize TokPi2 = 2
 tokSize TokReplLet = 4
-tokSize TokAnd   = 2
-tokSize TokOr    = 2
+tokSize TokAnd = 2
+tokSize TokOr = 2
+tokSize TokAs = 2
 tokSize (TokReplT s) = T.length s
 
 data Token
diff --git a/src/Syntax.hs b/src/Syntax.hs
index 9b99f16..b3d98e2 100644
--- a/src/Syntax.hs
+++ b/src/Syntax.hs
@@ -32,6 +32,14 @@ data WiredIn
 
   | WiPartial  -- (φ : I) -> Type           -> Typeω
   | WiPartialP -- (φ : I) -> Partial r Type -> Typeω
+
+  | WiSub      -- (A : Type) (φ : I) -> Partial φ A -> Typeω
+  | WiInS      -- {A : Type} {φ : I} (u : A) -> Sub A φ (λ x -> u)
+  | WiOutS     -- {A : Type} {φ : I} {u : Partial φ A} -> Sub A φ u -> A
+
+  | WiComp  --    {A : I -> Type} {phi : I}
+            -- -> ((i : I) -> Partial phi (A i)
+            -- -> (A i0)[phi -> u i0] -> (A i1)[phi -> u i1]
   deriving (Eq, Show, Ord)
 
 data Term
@@ -58,7 +66,7 @@ data Term
   -- ^ PathP : (A : I -> Type) -> A i0 -> A i1 -> Type
   | IElim     Term Term Term Term Term
   -- ^ IElim : {A : I -> Type} {x : A i0} {y : A i1} (p : PathP A x y) (i : I) -> A i
-  | PathIntro Term Term
+  | PathIntro Term Term Term Term
   -- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1)
   --   ~~~~~~~~~ not printed at all
 
@@ -71,6 +79,12 @@ data Term
   | PartialP Term Term
 
   | System (Map Term Term)
+
+  | Sub Term Term Term
+  | Inc Term Term Term
+  | Ouc Term Term Term Term
+
+  | Comp Term Term Term Term
   deriving (Eq, Show, Ord)
 
 data MV =
@@ -92,33 +106,40 @@ data Name
 
 type NFType = Value
 type NFEndp = Value
+type NFLine = Value
+type NFSort = Value
 
 data Value
-  = VNe    Head            (Seq Projection)
-  | VLam   Plicity         Closure
-  | VPi    Plicity Value   Closure
-  | VSigma Value   Closure
-  | VPair  Value   Value
+  = VNe    Head (Seq Projection)
+  | VLam   Plicity Closure
+  | VPi    Plicity Value Closure
+  | VSigma Value Closure
+  | VPair  Value Value
 
   | VType | VTypeω
 
   | VI
   | VI0 | VI1
-  | VIAnd Value Value
-  | VIOr  Value Value
-  | VINot Value
+  | VIAnd NFEndp NFEndp
+  | VIOr  NFEndp NFEndp
+  | VINot NFEndp
 
-  | VPath Value Value Value
-  | VLine Value Value
+  | VPath NFLine Value Value
+  | VLine NFLine Value Value Value
 
-  | VIsOne Value
+  | VIsOne NFEndp
   | VItIsOne
-  | VIsOne1 Value
-  | VIsOne2 Value
+  | VIsOne1 NFEndp
+  | VIsOne2 NFEndp
 
-  | VPartial NFEndp Value
+  | VPartial  NFEndp Value
   | VPartialP NFEndp Value
   | VSystem (Map Value Value)
+
+  | VSub NFSort NFEndp Value
+  | VInc NFSort NFEndp Value
+
+  | VComp NFSort NFEndp Value Value
   deriving (Eq, Show, Ord)
 
 pattern VVar :: Name -> Value
@@ -129,21 +150,22 @@ quoteWith names (VNe h sp) = foldl goSpine (goHead h) sp where
   goHead (HVar v) = Ref v
   goHead (HMeta m) = Meta m
 
-  goSpine t (PApp p v)       = App p t (quoteWith names v)
+  goSpine t (PApp p v) = App p t (quoteWith names v)
   goSpine t (PIElim l x y i) = IElim (quote l) (quote x) (quote y) t (quote i)
   goSpine t PProj1 = Proj1 t
   goSpine t PProj2 = Proj2 t
+  goSpine t (POuc a phi u) = Ouc (quote a) (quote phi) (quote u) t
 
 quoteWith names (VLam p (Closure n k)) =
-  let n' = refresh names n
+  let n' = refresh Nothing names n
    in Lam p n' (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
 
 quoteWith names (VPi p d (Closure n k)) =
-  let n' = refresh names n
+  let n' = refresh (Just d) names n
    in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
 
 quoteWith names (VSigma d (Closure n k)) =
-  let n' = refresh names n
+  let n' = refresh (Just d) names n
    in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
 
 quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
@@ -158,22 +180,26 @@ quoteWith names (VIOr x y) = IOr (quoteWith names x) (quoteWith names y)
 quoteWith names (VINot x) = INot (quoteWith names x)
 
 quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
-quoteWith names (VLine p f)      = PathIntro (quoteWith names p) (quoteWith names f)
+quoteWith names (VLine p x y f)  = PathIntro (quoteWith names p) (quoteWith names x) (quoteWith names y) (quoteWith names f)
 
 quoteWith names (VIsOne v)  = IsOne (quoteWith names v)
 quoteWith names (VIsOne1 v) = IsOne1 (quoteWith names v)
 quoteWith names (VIsOne2 v) = IsOne2 (quoteWith names v)
 quoteWith _     VItIsOne    = ItIsOne
 
-quoteWith names (VPartial x y) = Partial (quoteWith names x) (quoteWith names y)
-quoteWith names (VPartialP x y) = Partial (quoteWith names x) (quoteWith names y)
+quoteWith names (VPartial x y)  = Partial (quoteWith names x) (quoteWith names y)
+quoteWith names (VPartialP x y) = PartialP (quoteWith names x) (quoteWith names y)
 quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith names x, quoteWith names y)) (Map.toList fs)))
+quoteWith names (VSub a b c) = Sub (quoteWith names a) (quoteWith names b) (quoteWith names c)
+quoteWith names (VInc a b c) = Inc (quoteWith names a) (quoteWith names b) (quoteWith names c)
+quoteWith names (VComp a phi u a0) = Comp (quoteWith names a) (quoteWith names phi) (quoteWith names u) (quoteWith names a0)
 
-refresh :: Set Text -> Text -> Text
-refresh s n
+refresh :: Maybe Value -> Set Text -> Text -> Text
+refresh (Just VI) n _ = refresh Nothing n (T.pack "phi")
+refresh x s n
   | T.singleton '_' == n = n
   | n `Set.notMember` s = n
-  | otherwise = refresh s (n <> T.singleton '\'')
+  | otherwise = refresh x s (n <> T.singleton '\'')
 
 quote :: Value -> Term
 quote = quoteWith mempty
@@ -205,4 +231,5 @@ data Projection
   | PIElim Value Value Value NFEndp
   | PProj1
   | PProj2
+  | POuc   NFSort NFEndp Value 
   deriving (Eq, Show, Ord)
\ No newline at end of file
diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs
index f905688..60e083d 100644
--- a/src/Syntax/Pretty.hs
+++ b/src/Syntax/Pretty.hs
@@ -22,7 +22,10 @@ instance Pretty Name where
   pretty (Defined x)   = pretty x
 
 prettyTm :: Term -> Doc AnsiStyle
-prettyTm (Ref v) = pretty v
+prettyTm (Ref v) =
+  case T.uncons (getNameText v) of
+    Just ('.', w) -> keyword (pretty w)
+    _ -> pretty v
 
 prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x)
 prettyTm (App Ex f x) = parenFun f <+> parenArg x
@@ -33,7 +36,7 @@ prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
 
 prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> prettyTm bod where
   unwindLam (Lam p x y) = first ((p, x):) (unwindLam y)
-  unwindLam (PathIntro _ (Lam p x y)) = first ((p, x):) (unwindLam y)
+  unwindLam (PathIntro _ _ _ (Lam p x y)) = first ((p, x):) (unwindLam y)
   unwindLam t = ([], t)
 
   (al, bod) = unwindLam l
@@ -61,15 +64,19 @@ prettyTm (INot x) = operator (pretty '~') <> prettyTm x
 
 prettyTm (PathP l x y) = keyword (pretty "PathP") <+> parenArg l <+> parenArg x <+> parenArg y
 prettyTm (IElim _ _ _ f i) = prettyTm (App Ex f i)
-prettyTm (PathIntro _ f) = prettyTm f
+prettyTm (PathIntro _ _ _ f) = prettyTm f
 
-prettyTm (IsOne phi) = brackets (prettyTm phi)
-prettyTm ItIsOne = keyword (pretty "1=1")
-prettyTm (IsOne1 phi) = prettyTm (App Ex (Ref (Bound (T.pack "isOne1"))) phi)
-prettyTm (IsOne2 phi) = prettyTm (App Ex (Ref (Bound (T.pack "isOne2"))) phi)
+prettyTm (IsOne phi)  = prettyTm (App Ex (Ref (Bound (T.pack ".IsOne"))) phi)
+prettyTm ItIsOne      = keyword (pretty "1=1")
+prettyTm (IsOne1 phi) = prettyTm (App Ex (Ref (Bound (T.pack ".isOne1"))) phi)
+prettyTm (IsOne2 phi) = prettyTm (App Ex (Ref (Bound (T.pack ".isOne2"))) phi)
 
-prettyTm (Partial phi a)  = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack "Partial"))) [phi, a]
-prettyTm (PartialP phi a) = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack "PartialP"))) [phi, a]
+prettyTm (Partial phi a)   = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".Partial"))) [phi, a]
+prettyTm (PartialP phi a)  = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".PartialP"))) [phi, a]
+prettyTm (Comp a phi u a0) = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".comp"))) [a, phi, u, a0]
+prettyTm (Sub a phi u)     = prettyTm a <> brackets (prettyTm phi <+> operator (pretty "->") <+> prettyTm u)
+prettyTm (Inc _ _ u)       = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".inS"))) [u]
+prettyTm (Ouc _ _ _ u)     = prettyTm $ foldl (App Ex) (Ref (Bound (T.pack ".outS"))) [u]
 
 prettyTm (System xs) = braces (mempty <+> hsep (punctuate comma (map go (Map.toList xs))) <+> mempty) where
   go (f, t) = prettyTm f <+> operator (pretty "=>") <+> prettyTm t
@@ -83,10 +90,18 @@ operator = annotate (color Yellow)
 parenArg :: Term -> Doc AnsiStyle
 parenArg x@App{} = parens (prettyTm x)
 parenArg x@IElim{} = parens (prettyTm x)
+parenArg x@IsOne{} = parens $ prettyTm x
 parenArg x@IsOne1{} = parens $ prettyTm x
 parenArg x@IsOne2{} = parens $ prettyTm x
 parenArg x@Partial{} = parens $ prettyTm x
 parenArg x@PartialP{} = parens $ prettyTm x
+
+parenArg x@Sub{} = parens $ prettyTm x
+parenArg x@Inc{} = parens $ prettyTm x
+parenArg x@Ouc{} = parens $ prettyTm x
+
+parenArg x@Comp{} = parens $ prettyTm x
+
 parenArg x = prettyDom x
 
 prettyDom :: Term -> Doc AnsiStyle
@@ -107,4 +122,8 @@ showValue = L.unpack . renderLazy . layoutPretty defaultLayoutOptions . prettyTm
 
 showFace :: Map Head Bool -> Doc AnsiStyle
 showFace = hsep . map go . Map.toList where
-  go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
\ No newline at end of file
+  go (h, b) = parens $ prettyTm (quote (VNe h mempty)) <+> operator (pretty "=") <+> pretty (if b then "i1" else "i0")
+
+getNameText :: Name -> Text
+getNameText (Bound x) = x
+getNameText (Defined x) = x
\ No newline at end of file
diff --git a/test.tt b/test.tt
deleted file mode 100644
index 7513a6e..0000000
--- a/test.tt
+++ /dev/null
@@ -1,90 +0,0 @@
-{-# PRIMITIVE Type #-}
-{-# PRIMITIVE Pretype #-}
-
-I : Pretype
-{-# PRIMITIVE Interval I #-}
-
-i0 : I
-i1 : I
-{-# PRIMITIVE i0 #-}
-{-# PRIMITIVE i1 #-}
-
-iand : I -> I -> I
-{-# PRIMITIVE iand #-}
-
-ior : I -> I -> I
-{-# PRIMITIVE ior #-}
-
-inot : I -> I
-{-# PRIMITIVE inot #-}
-
-PathP : (A : I -> Pretype) -> A i0 -> A i1 -> Type
-{-# PRIMITIVE PathP #-}
-
-Path : {A : Pretype} -> A -> A -> Type
-Path {A} = PathP (\i -> A)
-
-refl : {A : Pretype} {x : A} -> Path x x
-refl {A} {x} i = x
-
-sym : {A : I -> Pretype} {x : A i0} {y : A i1} -> PathP A x y -> PathP (\i -> A (inot i)) y x
-sym p i = p (inot i)
-
-id : {A : Type} -> A -> A
-id x = x
-
-the : (A : Pretype) -> A -> A
-the A x = x
-
-iElim : {A : I -> Pretype} {x : A i0} {y : A i1} -> PathP A x y -> (i : I) -> A i
-iElim p i = p i
-
-Singl : (A : Type) -> A -> Type
-Singl A x = (y : A) * Path x y
-
-isContr : Type -> Type
-isContr A = (x : A) * ((y : A) -> Path x y)
-
-singContr : {A : Type} {a : A} -> isContr (Singl A a)
-singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))
-
-cong : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)
-cong f p i = f (p i)
-
-congComp : {A : Type} {B : Type} {C : Type}
-           {f : A -> B} {g : B -> C} {x : A} {y : A}
-           (p : Path x y)
-        -> Path (cong g (cong f p)) (cong (\x -> g (f x)) p)
-congComp p = refl
-
-congId : {A : Type} {x : A} {y : A}
-         (p : Path x y)
-     -> Path (cong (id {A}) p) p
-congId p = refl
-
-IsOne : I -> Type
-{-# PRIMITIVE IsOne #-}
-
-itIs1 : IsOne i1
-{-# PRIMITIVE itIs1 #-}
-
-isOneL : {i : I} {j : I} -> IsOne i -> IsOne (ior i j)
-{-# PRIMITIVE isOneL #-}
-
-isOneR : {i : I} {j : I} -> IsOne j -> IsOne (ior i j)
-{-# PRIMITIVE isOneR #-}
-
-Partial : I -> Type -> Pretype
-{-# PRIMITIVE Partial #-}
-
-PartialP : (phi : I) -> Partial phi Type -> Pretype
-{-# PRIMITIVE PartialP #-}
-
-Bool : Type
-tt, ff : Bool
-
-foo : (i : I) -> (j : I) -> Partial (ior (inot i) (ior i (iand i j))) Bool
-foo i j = \ { (i = i0) -> tt, (i = i1) -> ff, (i = i1) && (j = i1) -> ff }
-
-apPartial : {B : Type} {A : Type} -> (phi : I) -> (A -> B) -> Partial phi A -> Partial phi B
-apPartial phi f p is1 = f (p is1)
\ No newline at end of file