> module OTT where
> import Prelude hiding (EQ, pi)
> import GHC.Prim
> import Control.Applicative
> import Control.Monad
> import Control.Arrow
> import Data.Monoid
> import Data.Traversable
> import Data.Char
> import Data.Maybe


%-----------------------------------------------------------------------%
%   Syntax                                                              %
%-----------------------------------------------------------------------%

> data ExTm
>   = EI (InTm, InTm)
>   | ER Ref
>   | EV Int
>   | ET TCon [InTm]
>   | EPi (String, InTm) InTm
>   | EA ExTm InTm
>   | ERefl (InTm, InTm)
>   | EC Cop InTm InTm InTm InTm
>   | EP ExTm Int
>   | ES ExTm InTm [(String, InTm)]
>   deriving Show

> data TCon = Set | Q | E [String] deriving (Show, Eq)

> data Cop = Coe | Coh deriving (Show, Eq)

> data InTm
>   = IE ExTm
>   | ILam String InTm
>   | IQ [InTm]
>   | ID String
>   deriving Show

> type LiftedSub = (Int, Int -> ExTm)  -- must target Vclosed terms, natch

> lift :: LiftedSub -> LiftedSub
> lift (i, f) = (i + 1, f)

> substE :: LiftedSub -> ExTm -> ExTm
> substE sg (EI (tm, ty)) = EI (substI sg tm, substI sg ty)
> substE sg (ER r) = ER r
> substE (i, f) (EV x)
>   | j >= 0 = f j
>   | otherwise = EV x
>   where j = x - i
> substE sg (ET tc ts) = ET tc (fmap (substI sg) ts)
> substE sg (EPi (x, s) t) = EPi (x, substI sg s) (substI (lift sg) t)
> substE sg (EA f a) = EA (substE sg f) (substI sg a)
> substE sg (ERefl (tm, ty)) = ERefl (substI sg tm, substI sg ty)
> substE sg (EC cop s t q x) =
>   EC cop (substI sg s) (substI sg t) (substI sg q) (substI sg x)
> substE sg (EP t i) = EP (substE sg t) i
> substE sg (ES s p bs) =
>   ES (substE sg s) (substI sg p) (fmap (id *** (substI sg)) bs)

> substI :: LiftedSub -> InTm -> InTm
> substI sg (IE t) = IE (substE sg t)
> substI sg (ILam x b) = ILam x (substI (lift sg) b)
> substI sg (IQ ts) = IQ (fmap (substI sg) ts)
> substI sg (ID x) = ID x

> inst :: InTm -> ExTm -> InTm
> inst t s = substI (0, const s) t


%-----------------------------------------------------------------------%
%   Semantics                                                           %
%-----------------------------------------------------------------------%

> data Val
>   = VN Neut
>   | VPi (String, Val) (Val -> Val)
>   | VT TCon [Val]
>   | VLam String (Val -> Val)
>   | VQ [Val]                -- structural equality proofs
>   | VD String

> data Neut
>   = NR Ref                  -- a para
>   | NA Neut Val
>   | NC Cop Val Val Val Val  -- some cases missing, natch
>   | NP Neut Int
>   | NRefl (Val, Val)        -- reflexivity (an eq proof)
>   | NS Neut Val [(String, Val)]

> data Ref = Ref Name (Maybe Val) Val
> type Name = (String, Int)

> instance Show Ref where
>   show (Ref (x, 0) _ _) = x
>   show (Ref (x, i) _ _) = x ++ "_" ++ show i

> instance Eq Ref where
>   Ref x _ _ == Ref y _ _ = x == y

> vR :: Ref -> Val
> vR (Ref _ (Just v) _) = v
> vR r = VN (NR r)

> vA :: Val -> Val -> Val
> vA (VLam _ f) v           = f v
> vA (VN (NA (NA (NP r@(NRefl (f, VPi (_, s) t)) 0) x) y)) q | isRefl q =
>   VN (NRefl (vA f x, t x))  -- bonus compression
> vA (VN f) v               = VN (NA f v)

> isRefl :: Val -> Bool
> isRefl (VQ [])         = True
> isRefl (VN (NRefl _))  = True
> isRefl _               = False

> vC :: Cop -> Val -> Val -> Val -> Val -> Val
> vC Coe _ _ q x  | isRefl q = x                                 -- bonus
> vC Coh _ t q x  | isRefl q = VN (NRefl (x, t))                 -- bonus
> vC Coe (VT a []) (VT b []) _ x   | a == b = x
> vC Coh (VT a []) t@(VT b []) _ x | a == b = VN (NRefl (x, t))  -- bonus
> vC Coe (VPi (x0, s0) t0) (VPi (x1, s1) t1) q f0 = VLam x1 $ \v1 ->
>   let v0  = vC Coe s1 s0 (vP q 0) v1  -- only project from non-refl proofs
>       q10 = vC Coh s1 s0 (vP q 0) v1
>   in  vC Coe (t0 v0) (t1 v1) (vP q 1 `vA` v1 `vA` v0 `vA` q10) (f0 `vA` v0)
> vC cop s t q x = VN (NC cop s t q x)

> copType :: Cop -> Val -> Val -> Val -> Val -> Val
> copType Coe s t q x = t
> copType Coh s t q x = vEq (x, s) (vC Coe s t q x, t)

> vP :: Val -> Int -> Val
> vP (VQ vs)  i = vs !! i
> vP (VN n)   i = VN (NP n i)

> vSet :: Val
> vSet = VT Set []

> vEq :: (Val, Val) -> (Val, Val) -> Val
> vEq (tm0, ty0) (tm1, ty1) = VT Q [ty0, tm0, ty1, tm1]

> vS :: Val -> Val -> [(String, Val)] -> Val
> vS (VD x) _ bs | Just v <- lookup x bs = v
> vS (VN n) p bs = VN (NS n p bs)


%-----------------------------------------------------------------------%
%   Evaluation                                                          %
%-----------------------------------------------------------------------%

> class Eval t where
>   (?) :: [Val] -> t -> Val

> instance Eval ExTm where
>   g ? EI (tm, _)                = g ? tm
>   g ? ER r                      = vR r
>   g ? EV x                      = g !! x
>   g ? ET c ts                   = VT c (fmap (g ?) ts)
>   g ? EPi (x, d) r              = VPi (x, g ? d) $ \v -> (v : g) ? r
>   g ? EA f a                    = vA (g ? f) (g ? a)
>   g ? ERefl (tm, ty)            = VN (NRefl (g ? tm, g ? ty))
>   g ? EC cop s t q x            = vC cop (g ? s) (g ? t) (g ? q) (g ? x)
>   g ? EP t i                    = vP (g ? t) i
>   g ? ES s p bs                 = vS (g ? s) (g ? p) (fmap (id *** (g ?)) bs)

> instance Eval InTm where
>   g ? IE t      = g ? t
>   g ? ILam x b  = VLam x $ \v -> (v : g) ? b
>   g ? IQ ts     = VQ (fmap (g ?) ts)
>   g ? ID s      = VD s


%-----------------------------------------------------------------------%
%   Telescopes                                                          %
%-----------------------------------------------------------------------%

> data Tel = TNil | TCons Val (Val -> Tel)

> projType :: Tel -> Int -> Int -> Val -> Maybe Val
> projType (TCons s _) i j _ | i == j = return s
> projType (TCons _ t) i j v = projType (t (vP v i)) (i + 1) j v
> projType _ _ _ _ = Nothing

> telEq :: ([Val], Tel) -> ([Val], Tel) -> Tel
> telEq (tm0 : ts0, TCons ty0 tl0) (tm1 : ts1, TCons ty1 tl1) =
>   TCons (vEq (tm0, ty0) (tm1, ty1)) $ \_ ->  -- I fought hard for that _
>   telEq (ts0, tl0 tm0) (ts1, tl1 tm1)
> telEq _ _ = TNil

> tel :: TCon -> Tel
> tel Set = TNil
> tel (E _) = TNil
> tel Q =  TCons vSet $ \ty0 -> TCons ty0 $ \_ ->
>          TCons vSet $ \ty1 -> TCons ty1 $ \_ ->
>          TNil


%-----------------------------------------------------------------------%
%   Telescopes for Observational Equality                               %
%-----------------------------------------------------------------------%

> eqTel :: (Val, Val) -> (Val, Val) -> Maybe Tel
> eqTel (VPi (x0, s0) t0, VT Set []) (VPi (x1, s1) t1, VT Set []) = return $
>   TCons (vEq (s1, vSet) (s0, vSet)) $ \_ ->
>   TCons (
>     VPi (x1, s1) $ \v1 -> VPi (x0, s0) $ \v0 ->
>     VPi ("q", vEq (v1, s1) (v0, s0)) $ \_ -> vEq (t0 v0, vSet) (t1 v1, vSet)
>     ) $ \_ -> TNil
> eqTel (f0, VPi (x0, s0) t0) (f1, VPi (x1, s1) t1) = return $
>   TCons (
>     VPi (x0, s0) $ \v0 ->  VPi (x1, s1) $ \v1 ->
>     VPi ("q", vEq (v0, s0) (v1, s1)) $ \_ ->
>     vEq (vA f0 v0, t0 v0) (vA f1 v1, t1 v1)
>     ) $ \_ -> TNil
> eqTel  (VT Q [ty0, tm0, ty1, tm1], VT Set [])
>        (VT Q [ty2, tm2, ty3, tm3], VT Set []) =  return $ -- special case
>   TCons (vEq (tm0, ty0) (tm2, ty2)) $ \_ ->
>   TCons (vEq (tm1, ty1) (tm3, ty3)) $ \_ ->
>   TNil
> eqTel (VT a ts, VT Set []) (VT b us, VT Set []) | a == b = return $ 
>   telEq (ts, tel a) (us, tel a)
> eqTel (_, VT (E []) []) (_, VT (E []) []) = return TNil
> eqTel (VD x, VT (E xs) []) (VD y, VT (E ys) [])
>   | x == y && xs == ys = return TNil
>   | otherwise = return $
>     TCons (VT (E []) []) $ \_ -> TNil
> eqTel _ _ = Nothing


%-----------------------------------------------------------------------%
%   Bind a Variable (slightly dodgy)                                    %
%-----------------------------------------------------------------------%

> rX :: Int -> String -> Val -> Ref
> rX l x s = Ref (x, l) Nothing s


%-----------------------------------------------------------------------%
%   Definitional Equality                                               %
%-----------------------------------------------------------------------%

> equate :: Int -> Val -> Val -> Val -> Maybe ()
> equate l (VT Set []) (VT a as) (VT b bs) | a == b = equateTel l (tel a) as bs
> equate l (VT Set []) (VPi (x, s0) t0) (VPi (_, s1) t1) = do
>   equate l vSet s0 s1
>   let v = vR (rX l x s0)
>   equate (l + 1) vSet (t0 v) (t1 v)
> equate l (VPi (x, s) t) (VLam _ b) g = do
>   let v = vR (rX l x s)
>   equate (l + 1) vSet (b v) (vA g v)
> equate l (VPi (x, s) t) f (VLam _ b) = do
>   let v = vR (rX l x s)
>   equate (l + 1) vSet (vA f v) (b v)
> equate l (VT Q _) _ _ = return ()
> equate l (VT (E []) []) _ _ = return ()
> equate l (VT (E _) []) (VD x) (VD y) | x == y = return ()
> equate l ty (VN n0) (VN n1) = case neutEq l n0 n1 of
>   Just _ -> return ()
>   _ -> proofIrr l ty
> equate _ _ _ _ = Nothing

> equateTel :: Int -> Tel -> [Val] -> [Val] -> Maybe ()
> equateTel _ TNil [] [] = return ()
> equateTel l (TCons s t) (a : as) (b : bs) =
>   equate l s a b >> equateTel l (t a) as bs
> equateTel _ _ _ _ = Nothing

> proofIrr :: Int -> Val -> Maybe ()
> proofIrr l (VPi (x, s) t) = do
>   let v = vR (rX l x s)
>   proofIrr (l + 1) (t v)
> proofIrr l (VT Q _) = return ()
> proofIrr l (VT (E []) []) = return ()
> proofIrr _ _ = Nothing

> neutEq :: Int -> Neut -> Neut -> Maybe Val
> neutEq l (NR x@(Ref _ _ ty)) (NR y) = if x == y then return ty else Nothing
> neutEq l (NA f0 a0) (NA f1 a1) = do
>   VPi (_, s) t <- neutEq l f0 f1
>   equate l s a0 a1
>   return (t a0)
> neutEq l (NC Coe s t q (VN a)) b
>   | Just () <- equate l vSet s t = neutEq l a b
> neutEq l a (NC Coe s t q (VN b))
>   | Just () <- equate l vSet s t = neutEq l a b
> neutEq l (NC c0 s0 t0 q0 x0) (NC c1 s1 t1 q1 x1) | c0 == c1 = do
>   equate l vSet s0 s1
>   equate l vSet t0 t1
>   equate l (vEq (s0, vSet) (t0, vSet)) q0 q1
>   equate l s0 x0 x1
>   return t0
> neutEq l (NS s0 p0 []) (NS s1 p1 []) = do
>   equate l (VPi ("x", VT (E []) []) $ \_ -> vSet) p0 p1
>   return (vA p0 (VN s0))
> neutEq l (NS s0 p0 bs0) (NS s1 p1 bs1) = do
>   e@(VT (E xs) []) <- neutEq l s0 s1
>   equate l (VPi ("x", e) $ \_ -> vSet) p0 p1
>   for xs $ \x -> join $
>     equate l (vA p0 (VD x)) <$> lookup x bs0 <*> lookup x bs1
>   return (vA p0 (VN s0))
> neutEq _ _ _ = Nothing


%-----------------------------------------------------------------------%
%   Quotation                                                           %
%-----------------------------------------------------------------------%

> quoVa :: Int -> Val -> Val -> InTm
> quoVa l _ (VN t)          = IE (fst (quoNe l t))
> quoVa l _ (VT c ts)       = IE (ET c (quoTel l (tel c) ts))
> quoVa l _ (VPi (x, s) t)  =
>   IE (EPi (x, quoVa l vSet s) (quoVa (l + 1) vSet (t v)))
>   where v = vR (rX l "" s)
> quoVa l (VPi (_, s) t) (VLam x b) = ILam x (quoVa (l + 1) (t v) (b v))
>   where v = vR (rX l "" s)
> quoVa l (VT Q [ty0, tm0, ty1, tm1]) (VQ vs)
>   | Just tel <- eqTel (tm0, ty0) (tm1, ty1) =
>   IQ (quoTel l tel vs) where
> quoVa _ _ (VD s) = ID s

> quoTel :: Int -> Tel -> [Val] -> [InTm]
> quoTel l TNil [] = []
> quoTel l (TCons t tel) (v : vs) = quoVa l t v : quoTel l (tel v) vs

> quoNe :: Int -> Neut -> (ExTm, Val)
> quoNe l (NR (Ref ("", j) Nothing ty)) = (EV (l - j - 1), ty)
> quoNe l (NR r@(Ref _ _ ty)) = (ER r, ty)
> quoNe l (NA f a) =
>   let (f', VPi (_, s) t) = quoNe l f
>   in  (EA f' (quoVa l s a), t a)
> quoNe l (NRefl tty@(tm, ty)) =
>   let ty' = quoVa l vSet ty
>       tm' = quoVa l ty tm
>   in  (ERefl (tm', ty'), vEq tty tty)
> quoNe l (NC cop s t q (VN x)) | Just () <- equate l vSet s t = quoNe l x
> quoNe l (NC cop s t q x) =
>   let s' = quoVa l vSet s
>       t' = quoVa l vSet t
>       q' = quoVa l (vEq (s, vSet) (t, vSet)) q
>       x' = quoVa l s x
>   in  (EC cop s' t' q' x', copType cop s t q x)
> quoNe l (NP t i) =
>   let (t', VT Q [ty0, tm0, ty1, tm1]) = quoNe l t
>       Just tel = eqTel (tm0, ty0) (tm1, ty1)
>       Just ty = projType tel 0 i (VN t)
>   in  (EP t' i, ty)
> quoNe l (NS s p bs) =
>   let (s', e) = quoNe l s
>       p' = quoVa l (VPi ("x", e) $ \_ -> vSet) p
>       bs' = fmap (\(x, m) -> (x, quoVa l (vA p (VD x)) m)) bs
>   in  (ES s' p' bs', vA p (VN s))


%-----------------------------------------------------------------------%
%   Typechecking                                                        %
%-----------------------------------------------------------------------%

> exType :: Int -> ExTm -> Maybe (Val, Val)
> exType l (EI (tm', ty')) = do
>   ty <- inType l vSet ty'
>   tm <- inType l ty tm'
>   return (tm, ty)
> exType l (ER r@(Ref _ _ ty)) = return (vR r, ty)
> exType l (ET c ts') = do
>   ts <- inTel l (tel c) ts'
>   return (VT c ts, vSet)
> exType l e'@(EPi (x, s') t') = do
>   s <- inType l vSet s'
>   inType (l + 1) vSet (inst t' (ER (rX l x s)))
>   return ([] ? e', vSet)
> exType l (EA f' a') = do
>   (f, VPi (_, s) t) <- exType l f'
>   a <- inType l s a'
>   return (vA f a, t a)
> exType l (ERefl tty') = do
>   tty <- exType l (EI tty')
>   return (VN (NRefl tty), vEq tty tty)
> exType l (EC cop s' t' q' x') = do
>   s <- inType l vSet s'
>   t <- inType l vSet t'
>   q <- inType l (vEq (s, vSet) (t, vSet)) q'
>   x <- inType l s x'
>   return (vC cop s t q x, copType cop s t q x)
> exType l (EP t' i) = do
>   (t, VT Q [ty0, tm0, ty1, tm1]) <- exType l t'
>   tel <- eqTel (tm0, ty0) (tm1, ty1)
>   ty <- projType tel 0 i t
>   return (vP t i, ty)
> exType l (ES s' p' bs') = do
>   (s, e@(VT (E xs) [])) <- exType l s'
>   p <- inType l (VPi ("x", e) $ \_ -> vSet) p'
>   bs <- for xs $ \x -> ((,) x) <$> (inType l (vA p (VD x)) =<< lookup x bs')
>   return (vS s p bs, vA p s)

> inType :: Int -> Val -> InTm -> Maybe Val
> inType l want (IE tm') = do
>   (tm, got) <- exType l tm'
>   equate l vSet want got
>   return tm
> inType l (VPi (_, s) t) e'@(ILam x b') = do
>   let r = rX l x s
>   inType (l + 1) (t (vR r)) (inst b' (ER r))
>   return ([] ? e')
> inType l (VT Q [ty0, tm0, ty1, tm1]) (IQ ts') = do
>   qtel <- eqTel (tm0, ty0) (tm1, ty1)
>   ts <- inTel l qtel ts'
>   return (VQ ts)
> inType l (VT (E xs) []) (ID x) | elem x xs = return (VD x)
> inType _ _ _ = fail ""

> inTel :: Int -> Tel -> [InTm] -> Maybe [Val]
> inTel l TNil [] = return []
> inTel l (TCons tty tstel) (t' : ts') = do
>   t <- inType l tty t'
>   ts <- inTel l (tstel t) ts'
>   return (t : ts)
> inTel _ _ _ = Nothing


%-----------------------------------------------------------------------%
%   Test Rig                                                            %
%-----------------------------------------------------------------------%

> type PET = [String] -> ExTm
> type PIT = [String] -> InTm

> infixl 9 $>, $<
> class App f where
>   ($>) :: f -> [PIT] -> PET

> ($<) :: App f => f -> [PIT] -> PIT
> ($<) f as g = IE (($>) f as g)

> v :: App f => f -> PET
> v x = x $> []

> u :: App f => f -> PIT
> u x = x $< []

> instance App ExTm where
>   ($>) f as g = foldl EA f (fmap ($ g) as)

> instance App PET where
>   ($>) f as g = ($>) (f g) as g

> instance App String where
>   ($>) x as g = (EV (seek g) $> as) g where
>     seek (y : g) | x == y     = 0
>                  | otherwise  = 1 + seek g

> infix 5 <:

> (<:) :: PIT -> PIT -> PET
> (<:) tm ty g = EI (tm g, ty g)

> enum :: [String] -> PIT
> enum xs g = IE (ET (E xs) [])

> d :: String -> PIT
> d x g = ID x

> infixr 7 -->

> pi :: [(String, PIT)] -> PIT -> PIT
> pi [] t g = t g
> pi ((x, s) : xss) t g = IE (EPi (x, s g) (pi xss t (x : g)))

> (-->) :: PIT -> PIT -> PIT
> s --> t = pi [("", s)] t

> set :: PIT
> set g = IE (ET Set [])

> infixr 7 ==>

> (==>) :: [String] -> PIT -> PIT
> (==>) [] t g = t g
> (==>) (x : xs) t g = ILam x ((xs ==> t) (x : g))

> k :: PIT -> PIT
> k p = [""] ==> p

> infix 8 ===, *=*

> (===) :: (PIT, PIT) -> (PIT, PIT) -> PIT
> (===) (tm0, ty0) (tm1, ty1) g = IE (ET Q [ty0 g, tm0 g, ty1 g, tm1 g])

> (*=*) :: PIT -> PIT -> PIT
> s *=* t = (s, set) === (t, set)

> ec ::  Cop -> PIT -> PIT -> PIT -> PIT -> PIT
> ec cop s t q x g = IE (EC cop (s g) (t g) (q g) (x g))

> iq :: [PIT] -> PIT
> iq ps = IQ <$> sequenceA ps

> er :: (PIT, PIT) -> PET
> er (tm, ty) g = ERefl (tm g, ty g)

> ir :: (PIT, PIT) -> PIT
> ir (tm, ty) g = IE (ERefl (tm g, ty g))

> infixl 9 @@
> (@@) :: PET -> Int -> PET
> (@@) p i g = EP (p g) i

> switch :: PET -> PIT -> [(String, PIT)] -> PIT
> switch s p bs g = IE (ES (s g) (p g) (fmap (id *** ($ g)) bs))

> infix 3 +>
> (+>) = (,)

> try :: (PIT, PIT) -> Maybe (InTm, InTm)
> try (tm, ty) = do
>   (e, ty) <- exType 0 (EI (tm [], ty []))
>   return (quoVa 0 ty e, quoVa 0 vSet ty)

> define :: String -> [(String, PIT)] -> PIT -> PIT -> Ref
> define f as t b = fromJust $ do
>   (tm, ty) <- exType 0 (EI ((fmap fst as ==> b) [], pi as t []))
>   return $ Ref (f, 0) (Just tm) ty

> showDef :: Ref -> (InTm, InTm)
> showDef (Ref _ (Just tm) ty) = (quoVa 0 ty tm, quoVa 0 vSet ty)

> instance App Ref where
>   f $> as = (ER f) $> as


%-----------------------------------------------------------------------%
%   Just a Bit of Fun                                                   %
%-----------------------------------------------------------------------%

> bool :: Ref
> bool = define "bool" [] set $
>   enum ["tt", "ff"]

> bnot :: Ref
> bnot = define "bnot" [("b", u bool)] (u bool) $
>  switch (v "b") (k (u bool))
>  [ "tt" +> d "ff"
>  , "ff" +> d "tt"
>  ] 

> bid :: Ref
> bid = define "bid" [("b", u bool)] (u bool) $ u "b"

> bnotnot :: Ref
> bnotnot = define "bnotnot" [("b", u bool)] (u bool) $
>   bnot $< [bnot $< [u "b"]]

> trans :: Ref
> trans = define "trans"
>   [("A", set),("a", u "A"),("B", set),("b", u "B"),("C", set),("c",u "C")
>   ,("ab", (u "a", u "A") === (u "b", u "B"))
>   ,("bc", (u "b", u "B") === (u "c", u "C"))
>   ] ((u "a", u "A") === (u "c", u "C")) $
>   ec Coe  ((u "a", u "A") === (u "b", u "B"))
>           ((u "a", u "A") === (u "c", u "C"))
>           (iq [ir (u "a", u "A"), u "bc"])
>           (u "ab")

> ext :: Ref
> ext = define "ext"
>   [("S", set),("T", u "S" --> set)
>   ,("f", pi [("x", u "S")] ("T" $< [u "x"]))
>   ,("g", pi [("x", u "S")] ("T" $< [u "x"]))
>   ,("fg", pi [("x", u "S")]
>     (("f" $< [u "x"], "T" $< [u "x"]) === ("g" $< [u "x"], "T" $< [u "x"])))
>   ] ((u "f", pi [("x", u "S")] ("T" $< [u "x"])) ===
>      (u "g", pi [("x", u "S")] ("T" $< [u "x"]))) $
>   iq [["x", "y", "xy"] ==>
>     trans $< ["T" $< [u "x"], "f" $< [u "x"]
>              ,"T" $< [u "x"], "g" $< [u "x"]
>              ,"T" $< [u "y"], "g" $< [u "y"]
>              ,"fg" $< [u "x"]
>              ,er (u "g", pi [("x", u "S")] ("T" $< [u "x"])) @@ 0 $<
>                 [u "x", u "y", u "xy"]]]

> bnotnot_eq_bid :: Ref
> bnotnot_eq_bid = define "bnotnot_eq_bid" []
>   ((u bnotnot, u bool --> u bool) === (u bid, u bool --> u bool)) $
>   ext $< [u bool, k (u bool), u bnotnot, u bid, ["b"] ==>
>     switch (v "b")
>       (["b"] ==> ((bnotnot $< [u "b"], u bool) === (bid $< [u "b"], u bool)))
>       [ "tt" +> iq []
>       , "ff" +> iq []
>       ]]

> so :: Ref
> so = define "so" [("b", u bool)] set $
>   switch (v "b") (k set)
>   [ "tt" +> enum ["void"]
>   , "ff" +> enum []
>   ]

> fam :: Ref
> fam = define "fam" [("f", u bool --> u bool)] set $ so $< ["f" $< [d "tt"]]

> transport :: Ref
> transport = define "transport"
>   [("x", fam $< [u bnotnot])] (fam $< [u bid]) $
>   ec Coe (fam $< [u bnotnot]) (fam $< [u bid])
>     (er (u fam, (u bool --> u bool) --> set) @@ 0 $<
>       [u bnotnot, u bid, u bnotnot_eq_bid])
>     (u "x")