content: {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable,
      GADTs, DataKinds, KindSignatures, TypeOperators,
      TypeFamilies, TupleSections, PolyKinds, RankNTypes,
      MultiParamTypeClasses, FlexibleInstances, ScopedTypeVariables,
      StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}
  
  module KanGo where
  
  import Control.Monad
  import Control.Monad.Identity
  import Control.Applicative
  import Data.Maybe
  
  data SC  -- syntactic categories
     = TM  -- terms (checkable)
     | EL  -- eliminations (synthable)
     | PT  -- points
  
  data CX  -- contexts expose the syntactic categories of bound vars
     = C0
     | CX :\ SC
  
  data Var :: CX -> SC -> * where  -- de Bruijn indices for bound vars
    V0 :: Var (g :\ s) s
    VS :: Var g t -> Var (g :\ s) t
  deriving instance Eq (Var g s)
  
  data Syn :: CX -> SC -> * where
    I      :: Bit -> Syn g PT
    Mux    :: Syn g PT -> Syn g PT -> Syn g PT -> Syn g PT
  
    Type   :: Syn g TM
    
    B      :: Quant -> Syn g TM -> Bnd g EL -> Syn g TM
    L      :: Bnd g EL -> Syn g TM
    (:&)   :: Syn g TM -> Syn g TM -> Syn g TM
  
    (:-:)  :: Syn g TM -> Syn g TM -> Syn g TM
    Conn   :: Syn g TM -> Triple (Syn g TM) -> Syn g TM -> Syn g TM
    Path   :: Bnd g PT -> Syn g TM
    KanT   :: KAN (Syn g) -> Syn g TM
    Inter  :: INTERPOL (Syn g) -> Syn g TM
  
    E      :: Syn g EL -> Syn g TM
  
    V      :: Var g c -> Syn g c
    P      :: FV c -> Syn g c
  
    (:::)  :: Syn g TM -> Syn g TM -> Syn g EL
  
    (:$)   :: Syn g EL -> Syn g TM -> Syn g EL
    (:.)   :: Syn g EL -> Syn g PT -> Syn g EL
    (:@)   :: Syn g EL -> Bit -> Syn g EL
    (:^)   :: Syn g TM -> Triple (Syn g TM) -> Syn g EL
    KanV   :: Bit -> KAN (Syn g) -> Syn g TM -> Syn g EL
    InterV :: Bit -> INTERPOL (Syn g) -> Syn g TM -> Syn g EL
  deriving instance Eq (Syn g b)
  
  data Bnd :: CX -> SC -> * where
    R :: Nom -> Syn (g :\ b) TM -> Bnd g b   -- relevant
    K :: Syn g TM -> Bnd g b                    -- konstant
    deriving Eq
  
  newtype Nom = Nom {nom :: String}
  instance Show Nom where show = nom
  instance Eq Nom where _ == _ = True
  
  data Quant = Pi | Sg deriving Eq
  instance Show Quant where
    show Pi = "->"
    show Sg = "*"
  
  data Bit = B0 | B1 deriving Eq  -- I probably use these for too much
  instance Show Bit where
    show B0 = "0"
    show B1 = "1"
  
  data Pair x = Pr {
    thing0 :: x    ,
    thing1 :: x    }
    deriving (Functor, Foldable, Traversable, Eq)
  thing :: Bit -> Pair x -> x
  thing B0 = thing0
  thing B1 = thing1
  
  data Triple x = Tr  {
    point0 :: x       ,
    path01 :: x       ,
    point1 :: x       }
    deriving (Functor, Foldable, Traversable, Eq)
    -- to be used for two things joined by a path in the middle
  point :: Bit -> Triple x -> x
  point B0 = point0
  point B1 = point1
  
  data KAN f = KAN            {
    side0   :: Triple (f TM)  ,
    side1   :: Triple (f TM)  ,
    base    :: f TM           ,
    vert    :: f PT           ,
    horiz   :: f PT           }
  deriving instance Eq (KAN (Syn g))
  side :: Bit -> KAN f -> Triple (f TM)
  side B0 = side0
  side B1 = side1
  
  data INTERPOL f = INTERPOL {
    types  :: Pair (f TM)    ,  -- S                           T
    xports :: Pair (f TM)    ,  -- f : S -> T                  g : T -> S
    rtrips :: Pair (f TM)    ,  -- p : (s : S) -> f (g s) = s  q : (t : T) -> g (f t) = t
    triang :: Pair (f TM)    ,  -- (s : S) -> q (f s) = \ i -> g (p s i)
    coord  :: f PT           }  --                  (t : T) -> p (g t) = \ i -> f (q t i)
  deriving instance Eq (INTERPOL (Syn g))
  
  class Kit (t :: CX -> SC -> *) where
    vze   :: t (g :\ b) b
    tout  :: t g b -> Syn g b
    wk    :: t g b -> t (g :\ c) b
  
  instance Kit Var where
    vze   = V0
    tout  = V
    wk    = VS
  
  instance Kit Syn where
    vze   = V V0
    tout  = id
    wk    = ren VS
  
  act :: (Applicative f, Kit t) => (forall b. Var g b -> f (t d b)) ->
         Syn g b -> f (Syn d b)
  act f (I b)          = pure (I b)
  act f (Mux r s t)    = Mux <$> act f r <*> act f s <*> act f t
  act f Type           = pure Type
  act f (B q s t)      = B q <$> act f s <*> bact f t
  act f (L t)          = L <$> bact f t
  act f (s :& t)       = (:&) <$> act f s <*> act f t
  act f (s :-: t)      = (:-:) <$> act f s <*> act f t
  act f (Conn s q t)   = Conn <$> act f s <*> traverse (act f) q <*> act f t
  act f (Path t)       = Path <$> bact f t
  act f (KanT k)       = KanT <$> kact f k
  act f (Inter i)      = Inter <$> iact f i
  act f (E e)          = E <$> act f e
  act f (V i)          = tout <$> f i
  act f (P x)          = pure (P x)
  act f (g :$ s)       = (:$) <$> act f g <*> act f s
  act f (g :. p)       = (:.) <$> act f g <*> act f p
  act f (g :@ b)       = (:@) <$> act f g <*> pure b
  act f (g :^ q)       = (:^) <$> act f g <*> traverse (act f) q
  act f (KanV b k v)   = KanV b <$> kact f k <*> act f v
  act f (InterV b i v) = InterV b <$> iact f i <*> act f v
  
  kact :: (Applicative f, Kit t) => (forall b. Var g b -> f (t d b)) ->
          KAN (Syn g) -> f (KAN (Syn d))
  kact f (KAN s0 s1 b v h) =
    KAN <$> traverse (act f) s0 <*> traverse (act f) s1 <*> act f b
        <*> act f v <*> act f h
  
  iact :: (Applicative f, Kit t) => (forall b. Var g b -> f (t d b)) ->
          INTERPOL (Syn g) -> f (INTERPOL (Syn d))
  iact f (INTERPOL st fg pq hk i) =
    INTERPOL <$> traverse (act f) st <*> traverse (act f) fg
             <*> traverse (act f) pq <*> traverse (act f) hk
             <*> act f i
  
  bact :: forall f t g d c. (Applicative f, Kit t) =>
         (forall b. Var g b -> f (t d b)) ->
         Bnd g c -> f (Bnd d c)
  bact f (R x t) = R x <$> act g t where
    g :: forall b. Var (g :\ c) b -> f (t (d :\ c) b)
    g V0 = pure vze
    g (VS i) = wk <$> f i
  bact f (K t) = K <$> act f t
  
  ren :: (forall b. Var g b -> Var d b) -> Syn g b -> Syn d b
  ren f = runIdentity . act (Identity . f)
  
  dep :: Bnd g b -> Either (Syn g TM) (Syn (g :\ b) TM)
  dep (K t)   = Left t
  dep (R x t) = case act str t of
      Just t  -> Left t
      Nothing -> Right t
    where
      str :: Var (g :\ b) c -> Maybe (Var g c)
      str V0     = Nothing
      str (VS i) = Just i
  
  bnd :: String -> Syn (g :\ b) TM -> Bnd g b
  bnd x t = case dep b of
      Left t  -> K t
      Right _ -> b
    where b = R (Nom x) t
    -- could add thickening?
  
  data Sem :: SC -> * where
    VI      :: Bit -> Sem PT
    VMux    :: FV PT -> Sem PT -> Sem PT -> Sem PT
  
    VType   :: Sem TM
    
    VB      :: Quant -> Sem TM -> Clo EL -> Sem TM
    VL      :: Clo EL -> Sem TM
    (::&)   :: Sem TM -> Sem TM -> Sem TM
  
    (::-:)  :: Sem TM -> Sem TM -> Sem TM
    VConn   :: Sem TM -> Triple (Sem TM) -> Sem TM -> Sem TM
    VPath   :: Clo PT -> Sem TM
    VKanT   :: KAN Sem -> Sem TM
    VInter  :: INTERPOL Sem -> Sem TM
  
    N       :: Sem EL -> Sem TM
  
    X       :: FV EL -> Sem EL
  
    (::$)   :: Sem EL -> Sem TM -> Sem EL
    (::.)   :: Sem EL -> Sem PT -> Sem EL
    (::@)   :: Sem EL -> Bit -> Sem EL
    (::^)   :: Sem TM -> Triple (Sem TM) -> Sem EL
    VKanV   :: Bit -> KAN Sem -> Sem TM -> Sem EL
    VInterV :: Bit -> INTERPOL Sem -> Sem TM -> Sem EL
  
  data Env :: CX -> * where
    E0   :: Env C0
    (:<) :: Env g -> Val b -> Env (g :\ b)
  
  data Clo :: SC -> * where
    VR :: Env g -> Nom -> Syn (g :\ b) TM -> Clo b  -- relevant
    VK :: Sem TM -> Clo b                              -- konstant
  
  data FV :: SC -> * where
    Dim :: Int -> Nom -> FV PT
    Par :: Int -> Sem TM -> Nom -> FV EL
  
  nomC :: Clo b -> String
  nomC (VR _ x _) = nom x
  nomC _ = "x"
  
  
  -- Semantically, this is what we expect to get when
  -- we eval whatever it is.
  
  type family Val (c :: SC) :: * where
    Val PT = Sem PT
    Val EL = (Sem TM, Sem TM)  -- (val, type)
    Val TM = Sem TM
  
  -- semantically, everything needs a name supply;
  -- we work in (Int ->)
  
  stan :: Clo b -> Val b -> Int -> Val TM
  stan (VR g _ b) v = eval (g :< v) b
  stan (VK t)     _ = pure t
  
  instance Ord (FV PT) where
    compare (Dim i _) (Dim j _) = compare i j
  
  instance Eq (FV c) where
    Dim i _   == Dim j _    = i == j
    Par i _ _ == Par j _ _  = i == j
  
  dim :: FV PT -> Val PT
  dim i = VMux i (VI B0) (VI B1)
  
  eval :: Env g -> Syn g b -> Int -> Val b
  eval _ (I b) = pure (VI b)
  eval g (Mux c p0 p1) = mux <$> eval g c <*> eval g p0 <*> eval g p1
  eval _ Type  = pure VType
  eval g (B q s t) = VB q <$> eval g s <*> clo g t
  eval g (L b) = VL <$> clo g b
  eval g (s :& t) = (::&) <$> eval g s <*> eval g t
  eval g (s :-: t) = (::-:) <$> eval g s <*> eval g t
  eval g (Conn s q t) = VConn <$> eval g s <*> traverse (eval g) q <*> eval g t
  eval g (Path b) = VPath <$> clo g b
  eval g (KanT k) = kan =<< keval g k
  eval g (Inter i) = inter =<< ieval g i
  eval g (E e) = fst <$> eval g e
  eval g (V i) = pure (proj g i)
  eval _ (P i@(Dim _ _)) = pure (dim i)
  eval _ (P x@(Par i t _)) = pure (N (X x), t)
  eval g (t ::: tT) = (,) <$> eval g t <*> eval g tT
  eval g (f :$ s) = join (apf <$> eval g f <*> eval g s)
  eval g (f :. p) = do
    qQ@(vq, vQ) <- eval g f
    vp <- eval g p
    case vQ of
      vS ::-: vT -> (, VType) <$> apa (Tr vS vq vT) vp
      VConn vs vP vt -> (,) <$> apa (Tr vs vq vt) vp <*> apa vP vp
  eval g (e :@ b) = join (field b <$> eval g e)
  eval g (r :^ q) = do
    r <- eval g r
    p <- traverse (eval g) q
    (, point1 p) <$> transport r p
  
  idFun :: Sem TM
  idFun = VL (VR E0 (Nom "") (E (V V0)))
  
  stretch :: Sem TM -> Triple (Sem TM)
  stretch vx = Tr vx (VPath (VK vx)) vx
  
  interDeg :: INTERPOL Sem -> Int -> Bool
  interDeg (INTERPOL (Pr vS vT) (Pr vf vg) (Pr vp vq) (Pr vh vk) i) = do
    pqT <- piTy "s" vS $ \ vs -> pure (VConn vs (stretch vS) vs)
    pqF <- lam pqT "s" $ \ vs -> pure (VPath (VK vs))
    hkT <- piTy "s" vS $ \ vs -> pure (VConn (VPath (VK vs))
                                             (stretch (VConn vs (stretch vS) vs))
                                             (VPath (VK vs)))
    hkF <- lam hkT "s" $ \ vs -> pure (VPath (VK (VPath (VK vs))))
    bs <- sequenceA
      [ equal VType vS vT
      , equal (vS ->> vS) vf idFun , equal (vS ->> vS) vg idFun
      , equal pqT vp pqF           , equal pqT vq pqF
      , equal hkT vh hkF           , equal hkT vk hkF
      ]
    pure $ all id bs
    
  inter :: INTERPOL Sem -> Int -> Sem TM
  inter i@(INTERPOL st _ _ _ (VI b)) = pure $ thing b st
  inter i = do
    b <- interDeg i
    pure $ if b then thing0 (types i) else VInter i
  
  (->>) :: Sem TM -> Sem TM -> Sem TM
  vS ->> vT = VB Pi vS (VK vT)
  
  interV :: Bit {- B0 from point j to 0 (i.e., S); B1 from 0 to point j -} ->
            INTERPOL Sem -> Sem TM -> Int -> Sem TM
  interV du i@(INTERPOL st@(Pr vS vT) fg@(Pr vf vg) pq hk j) v = do
    b <- interDeg i
    if b then pure v else case (du, j) of
      (_,  VI B0)  -> pure v   -- we're already at S; up and down are both trivial
      (B0, VI B1)  -> fst <$> apf (vg, vT ->> vS) v
      (B1, VI B1)  -> fst <$> apf (vf, vS ->> vT) v
      _            -> pure (N (VInterV du i v))
  
  keval :: Env g -> KAN (Syn g) -> Int -> KAN Sem
  keval g (KAN s0 s1 b v h) =
    KAN <$> traverse (eval g) s0 <*> traverse (eval g) s1 <*> eval g b
        <*> eval g v <*> eval g h
  
  ieval :: Env g -> INTERPOL (Syn g) -> Int -> INTERPOL Sem
  ieval g (INTERPOL st fg pq hk i) =
    INTERPOL <$> traverse (eval g) st <*> traverse (eval g) fg
             <*> traverse (eval g) pq <*> traverse (eval g) hk
             <*> eval g i
  
  piTy :: String -> Sem TM -> (Sem TM -> Int -> Sem TM) -> Int -> Sem TM
  piTy n vS f = underEL vS $ \ x -> do
    let vx = N (X x)
    vT <- f vx
    tT <- quote (Q0 :\\ x) VType vT
    VB Pi vS <$> clo E0 (bnd n tT)
  
  lam :: Sem TM -> String -> (Sem TM -> Int -> Sem TM) -> Int -> Sem TM
  lam (VB Pi vS cT) n f = underEL vS $ \ x -> do
    let vx = N (X x)
    vt <- f vx
    vT <- stan cT (vx, vS)
    t <- quote (Q0 :\\ x) vT vt
    VL <$> clo E0 (bnd n t)
  
  path :: String -> (Sem PT -> Int -> Sem TM) -> Int -> Sem TM
  path x p = underPT $ \ i -> do
    vT <- p (dim i)
    tT <- quote (Q0 :\\ i) VType vT
    VPath <$> clo E0 (bnd x tT)
  
  vpath :: Triple (Sem TM) -> String -> (Sem PT -> Int -> Sem TM) -> Int -> Sem TM
  vpath vQ x p = underPT $ \ i -> do
    vT <- apa vQ (dim i)
    vt <- p (dim i)
    t  <- quote (Q0 :\\ i) vT vt
    VPath <$> clo E0 (bnd x t)
  
  segment :: Triple (Sem TM) -> Sem PT -> Sem PT -> Int -> Triple (Sem TM)
  segment p i j = Tr <$> apa p i <*> path "k" (\ k -> apa p (mux k i j)) <*> apa p j
  
  synpa :: Syn (C0 :\ PT) TM -> Int -> Sem TM
  synpa b = eval E0 (Path (bnd "i" b))
  
  transport :: Val TM -> Triple (Sem TM) -> Int -> Sem TM
  transport vr (Tr _ (VPath (VK _)) _) = pure vr  -- *obviously* degenerate
  transport vr p = underPT $ \ h -> do
    vZ <- apa p (dim h)
    zZ <- quote (Q0 :\\ h) VType vZ  -- obtain syntax of typical point
    case dep (R (Nom "i") zZ) of
      Left _  -> pure vr -- *detectably* degenerate
      Right _ -> case (point0 p, zZ, point1 p) of
        (vR@(VB Sg vS0 cT0), B Sg sS tT, VB Sg vS1 cT1) -> do
          pS <- Tr vS0 <$> synpa sS <*> pure vS1
          (vs0, _) <- field B0 (vr, vR)
          let vs i = transport vs0 =<< segment pS (VI B0) i
              vT i = do
                cT <- clo (E0 :< i) tT
                stan cT =<< ((,) <$> vs i <*> apa pS i)
          (vt0, vT0) <- field B1 (vr, vR)
          (::&) <$> vs (VI B1)
                <*> (transport vt0 =<< (Tr vT0 <$> path "i" vT <*> vT (VI B1)))
        (vR@(VB Pi vS0 cT0), B Pi sS tT, vU@(VB Pi vS1 cT1)) ->
          lam vU (nomC cT1) $ \ vs1 -> do
            pS <- Tr vS0 <$> synpa sS <*> pure vS1
            let vs i = transport vs1 =<< segment pS (VI B1) i
                vT i = do
                  cT <- clo (E0 :< i) tT
                  stan cT =<< ((,) <$> vs i <*> apa pS i)
            (vt0, vT0) <- apf (vr, vR) =<< vs (VI B0)
            transport vt0 =<< (Tr vT0 <$> path "i" vT <*> vT (VI B1))
        (vS0 ::-: vT0, sS :-: tT, vS1 ::-: vT1) -> path "j" $ \ j -> do
          vS <- synpa sS
          vT <- synpa tT
          kan (KAN { side0 = Tr vS0 vS vS1
                   , base  = vr
                   , side1 = Tr vT0 vT vT1
                   , vert  = VI B1
                   , horiz = j})
        (VConn vs0 vQ0 vt0, Conn s qQ t, VConn vs1 vQ1 vt1) -> do
          let vQ i = traverse (eval (E0 :< i)) qQ
          path "j" $ \ j -> do
            vp0 <- apa (Tr vs0 vr vt0) j
            vQj <- path "i" $ \ i -> do
              vQi <- vQ i
              apa vQi j
            transport vp0 =<< (Tr <$> apa vQ0 j <*> pure vQj <*> apa vQ1 j)
        (_, KanT k@(KAN s0 s1 b v h), _) -> do -- faces may be degenerate...
          vk0 <- keval (E0 :< VI B0) k  -- ...so find them by instantiation
          vk1 <- keval (E0 :< VI B1) k
          vs0 <- kanV B0 vk0 vr   -- down the left face...
          let pB = VPath (VR E0 (Nom "i")
                     (E ((b ::: (point0 s0 :-: point0 s1)) :. h)))
          -- ...across the base...
          vs1 <- transport vs0 =<< (Tr <$> apa (kanB vk0) (horiz vk0)
                                       <*> pure pB
                                       <*> apa (kanB vk1) (horiz vk1))
          kanV B1 vk1 vs1  -- ...and up the right face
        (_, Inter i@(INTERPOL (Pr sS _) _ _ _ _), _) -> do
          vi0 <- ieval (E0 :< VI B0) i
          vi1 <- ieval (E0 :< VI B1) i
          vs0 <- interV B0 vi0 vr  -- down from interpolant to S0
          pS <- Tr (thing0 (types vi0)) <$> synpa sS <*>
              pure (thing0 (types vi1))
          -- from S0 to S1
          vs1 <- transport vs0 pS
          interV B1 vi1 vs1  -- up from S1 to interpolant
        _ -> pure (N (vr ::^ p))
  
  kanB :: KAN Sem -> Triple (Sem TM)
  kanB (KAN (Tr vS _ _) (Tr vT _ _) b _ _) = Tr vS b vT
  
  -- trying to ship a value from a point in a Kan square
  --   (B0) down to the base
  --   (B1) or up from the base
  -- must do same degeneracy tests as kan, to keep sync
  kanV :: Bit -> KAN Sem -> Sem TM -> Int -> Sem TM
  kanV _ k v | pteq (vert k) (VI B0) = pure v   -- on the base already
  kanV du k v = case horiz k of
      VI b -> transport v =<< seg du (side b k)   -- on one side or the other
      _ -> do
        b <- (&&) <$> degenerate (side0 k) <*> degenerate (side1 k)
        pure $ if b then v else N (VKanV du k v)
    where
      seg B0 s = segment s (vert k) (VI B0)
      seg B1 s = segment s (VI B0) (vert k)
  
  degenerate :: Triple (Sem TM) -> Int -> Bool
  degenerate path = underPT $ \ i -> do
    vS <- apa path (dim i)
    sS <- quote (Q0 :\\ i) VType vS
    case bnd "i" sS of
      K _   -> pure True
      R _ _ -> pure False
  
  kan :: KAN Sem -> Int -> Sem TM
  kan k | pteq (vert k) (VI B0) = apa (kanB k) (horiz k)  -- on the base?
  kan k = case horiz k of
    VI b -> apa (side b k) (vert k)  -- one one side or the other
    _ -> do -- so we're in the interior...if there is an interior
      b <- (&&) <$> degenerate (side0 k) <*> degenerate (side1 k)
      if b then apa (kanB k) (horiz k) else pure $ VKanT k
  
  field :: Bit -> Val EL -> Int -> Val EL
  field B0 (s ::& _, VB Sg sS _)  = pure (s,            sS)
  field B0 (N e,     VB Sg sS _)  = pure (N (e ::@ B0), sS)
  field B1 (s ::& t, VB Sg sS tT) = (t,) <$> stan tT (s, sS)
  field B1 (N e,     VB Sg sS tT) = (N (e ::@ B1),) <$> stan tT (N (e ::@ B0), sS)
  
  apa :: Triple (Sem TM) -> Sem PT -> Int -> Sem TM
  apa (Tr vS _ _) (VI B0)   = pure vS
  apa (Tr _ _ vT) (VI B1)   = pure vT
  apa (Tr _ (VPath b) _) i  = stan b i
  apa (Tr _ (N f)     _) i  = pure (N (f ::. i))
  
  apf :: Val EL -> Val TM -> Int -> Val EL
  apf (f, VB Pi sS tT) s =
    let vs = (s, sS)
        vT = stan tT vs
        vt = case f of
               VL b -> stan b vs
               N f  -> pure (N (f ::$ s))
    in  (,) <$> vt <*> vT
    
  proj :: Env g -> Var g b -> Val b
  proj (_ :< v) V0 = v
  proj (g :< _) (VS i) = proj g i
  
  clo :: Env g -> Bnd g b -> Int -> Clo b
  clo g (R x b) = pure (VR g x b)
  clo g (K t)   = VK <$> eval g t
  
  mux :: Sem PT -> Sem PT -> Sem PT -> Sem PT
  mux (VI B0) p0 _ = p0
  mux (VI B1) _ p1 = p1
  mux (VMux i q0 q1) p0 p1 = vmux i (mux q0 p0 p1) (mux q1 p0 p1)
  
  vmux :: FV PT -> Sem PT -> Sem PT -> Sem PT
  vmux i p0 p1 | pteq p0 p1 = p0
  vmux i (VMux j q0 q1) p1
    | i == j  = vmux i q0 p1
    | i < j   = vmux j (vmux i q0 p1) (vmux i q1 p1)
  vmux i p0 (VMux j q0 q1)
    | i == j  = vmux i p0 q1
    | i < j   = vmux j (vmux i p0 q0) (vmux i p0 q1)
  vmux i p0 p1 = VMux i p0 p1
  
  pteq :: Sem PT -> Sem PT -> Bool
  pteq (VI b) (VI c) = b == c
  pteq (VMux i p0 p1) (VMux j q0 q1) =
    i == j && pteq p0 q0 && pteq p1 q1
  pteq _ _ = False
  
  data QJ :: CX -> * where
    Q0 :: QJ C0
    (:\\) :: QJ g -> FV b -> QJ (g :\ b)
  
  data (:~:) :: t -> t -> * where
    Refl :: t :~: t
  
  fveq :: FV a -> FV b -> Maybe (a :~: b)
  fveq (Dim i _) (Dim j _) | i == j = Just Refl
  fveq (Par i _ _) (Par j _ _) | i == j = Just Refl
  fveq _ _ = Nothing
  
  dbFV :: QJ g -> FV b -> Maybe (Var g b)
  dbFV Q0 _ = Nothing
  dbFV (q :\\ x) y = case fveq x y of
    Just Refl -> pure V0
    _         -> VS <$> dbFV q y
  
  equal :: Sem TM -> Sem TM -> Sem TM -> Int -> Bool
  equal vT vt0 vt1 = do
    t0 <- quote Q0 vT vt0
    t1 <- quote Q0 vT vt1
    pure (t0 == t1)
  
  underEL :: Sem TM -> (FV EL -> Int -> x) -> Int -> x
  underEL vS k i = k (Par i vS (Nom "")) (i + 1)
  
  underPT :: (FV PT -> Int -> x) -> Int -> x
  underPT k i = k (Dim i (Nom "")) (i + 1)
  
  quote :: QJ g -> Sem TM -> Sem TM -> Int -> Syn g TM
  quote q VType VType         = pure Type
  quote q VType (VB z vS cT)  = B z <$> quote q VType vS <*>
    (underEL vS $ \ x -> do
      vx <- eval E0 (P x)
      vT <- stan cT vx
      bnd (nomC cT) <$> quote (q :\\ x) VType vT)
  quote q VType (vS ::-: vT) = (:-:) <$> quote q VType vS <*> quote q VType vT
  quote q VType (VConn vs vP vt) =
    Conn <$> quote q (point0 vP) vs <*> quotr q vP <*> quote q (point1 vP) vt
  quote q VType (VKanT k) = KanT <$> quoka q k
  quote q VType (VInter i) = Inter <$> quoin q i
  quote q vF@(VB Pi vS cT) vf = underEL vS $ \ x -> do
      (vt, vT) <- apf (vf, vF) (N (X x))
      let n = case vf of
                VL (VR _ y _) -> nom y
                _ -> nomC cT
      L <$> (bnd n <$> quote (q :\\ x) vT vt)
  quote q vP@(VB Sg vS cT) vp = do
    (vs, vS) <- field B0 (vp, vP)
    (vt, vT) <- field B1 (vp, vP)
    (:&) <$> quote q vS vs <*> quote q vT vt
  quote q (vS ::-: vT) vq = underPT $ \ i -> do
    vS <- apa (Tr vS vq vT) =<< eval E0 (P i)
    Path <$> (bnd "i" <$> quote (q :\\ i) VType vS)
  quote q (VConn vs vQ vt) vq = underPT $ \ i -> do
    vi <- eval E0 (P i)
    vP <- apa vQ vi
    vp <- apa (Tr vs vq vt) vi
    Path <$> (bnd "i" <$> quote (q :\\ i) vP vp)
    
  quote q _ (N e) = E <$> (fst <$> quoel q e)
  quote q t _ = \ i -> error $ "YUK! " ++ display B1 q (quote q VType t i)
  
  quoka :: QJ g -> KAN Sem -> Int -> KAN (Syn g)
  quoka q (KAN s0@(Tr vS0 _ _) s1@(Tr vS1 _ _) b v h) =
    KAN <$> quotr q s0 <*> quotr q s1 <*> quote q (vS0 ::-: vS1) b
        <*> pure (quopt q v) <*> pure (quopt q h)
  
  hConn :: Sem TM -> Sem TM -> Sem TM -> Sem TM
  hConn vT vt0 vt1 = VConn vt0 (stretch vT) vt1
  
  quoin :: QJ g -> INTERPOL Sem -> Int -> INTERPOL (Syn g)
  quoin q (INTERPOL (Pr vS vT) (Pr vf vg) (Pr vp vq) (Pr vh vk) vi) = do
    let rf vs = fst <$> apf (vf, vS ->> vT) vs
        rg vt = fst <$> apf (vg, vT ->> vS) vt
    vpTy <- piTy "s" vS $ \ vs -> hConn vS <$> (rg =<< rf vs) <*> pure vs
    vqTy <- piTy "t" vT $ \ vt -> hConn vT <$> (rf =<< rg vt) <*> pure vt
    let rp vs = fst <$> apf (vp, vpTy) vs
        rq vt = fst <$> apf (vq, vqTy) vt
    vhTy <- piTy "s" vS $ \ vs ->
      hConn <$> (hConn vT <$> (rf =<< (rg =<< rf vs)) <*> rf vs)
            <*> (rq =<< rf vs)
            <*> (vpath (stretch vT) "i" $ \ i -> do
                  z <- Tr <$> (rg =<< rf vs) <*> rp vs <*> pure vs
                  rf =<< apa z i)
    vkTy <- piTy "st" vT $ \ vt ->
      hConn <$> (hConn vS <$> (rg =<< (rf =<< rg vt)) <*> rg vt)
            <*> (rp =<< rg vt)
            <*> (vpath (stretch vS) "i" $ \ i -> do
                  z <- Tr <$> (rf =<< rg vt) <*> rq vt <*> pure vt
                  rg =<< apa z i)
    INTERPOL <$> (Pr <$> quote q VType vS        <*> quote q VType vT)
             <*> (Pr <$> quote q (vS ->> vT) vf  <*> quote q (vT ->> vS) vg)
             <*> (Pr <$> quote q vpTy vp         <*> quote q vqTy vq)
             <*> (Pr <$> quote q vhTy vh         <*> quote q vkTy vk)
             <*> pure (quopt q vi)
  
  quotr :: QJ g -> Triple (Sem TM) -> Int -> Triple (Syn g TM)
  quotr q (Tr vS0 qS vS1) =
    Tr <$> quote q VType vS0 <*> quote q (vS0 ::-: vS1) qS <*> quote q VType vS1
  
  quoel :: QJ g -> Sem EL -> Int -> (Syn g EL, Sem TM)
  quoel q (X x@(Par _ vT _)) = case dbFV q x of
    Just i   -> pure (V i, vT)
    Nothing  -> pure (P x, vT)
  quoel q (vf ::$ vs) = do
    (f, VB Pi vS cT) <- quoel q vf
    (,) <$> ((f :$) <$> quote q vS vs)
        <*> stan cT (vs, vS)
  quoel q (vf ::. vp) = do
    (f, vF) <- quoel q vf
    case vF of
      vS ::-: vT -> pure $ (f :. quopt q vp, VType)
      VConn vs vP vt -> (f :. quopt q vp,) <$> apa vP vp
  quoel q (ve ::@ b) = do
    (e, vE@(VB Sg vS cT)) <- quoel q ve
    (_, vT) <- field b (N ve, vE)
    pure (e :@ b, vT)
  quoel q (vr ::^ vp) =
    (,) <$> ((:^) <$> quote q (point0 vp) vr <*> quotr q vp)
        <*> pure (point1 vp)
  quoel q (VKanV du vk vv) = do
    k <- quoka q vk
    vB <- apa (kanB vk) (horiz vk)
    let (src, trg) = case du of
          B0 -> (VKanT vk, vB)  -- if we're quoting, vk is nondegenerate
          B1 -> (vB, VKanT vk)
    v <- quote q src vv
    pure (KanV du k v, trg)
  quoel q (VInterV du vi vv) = do
    i <- quoin q vi
    let vS = thing0 (types vi)
        (src, trg) = case du of
          B0 -> (VInter vi, vS)
          B1 -> (vS, VInter vi)
    v <- quote q src vv
    pure (InterV du i v, trg)
  
  quopt :: QJ g -> Sem PT -> Syn g PT
  quopt q (VI b) = I b
  quopt q (VMux x p0 p1) = Mux p (quopt q p0) (quopt q p1) where
    p = case dbFV q x of
          Just i   -> V i
          Nothing  -> P x
  
  display :: Bit {- B1 is big; B0 is small -} -> QJ g -> Syn g b -> String
  
  display z q (Mux i (I B0) (I B1)) = display z q i
  display z q (Mux i (I B1) (I B0)) = "!" ++ display z q i
  display z q (E e) = display z q e
  display z q (V i) = display z q (P (qproj q i))
  
  display _ q (I b) = show b
  display _ q Type = "Type"
  display _ q (P (Dim _ i)) = show i
  display _ q (P (Par _ _ x)) = show x
  
  display B0 q t = "(" ++ display B1 q t ++ ")"
  
  display _ q (Mux i j k) = concat
    [display B0 q j, "<", display B1 q i, ">", display B0 q k]
  display _ q (B b s (K t)) = concat
    [display B0 q s, " ", show b, " ", display B1 q t]
  display _ q (B b s (R x t)) = concat
    ["(", y, " : ", display B1 q s, ") ", show b, " " ,display B1 (glomE q y) t]
    where y = freshen q (nom x)
  display _ q (L (K t)) = "\\ _ -> " ++ display B1 q t
  display _ q (L (R x t)) = concat ["\\ ", y, " -> ", display B1 (glomE q y) t]
    where y = freshen q (nom x)
  display _ q (s :& t) = display B0 q s ++ ", " ++ display B1 q t
  display _ q (s :-: t) = display B0 q s ++ " - " ++ display B0 q t
  display _ q (Conn s p t) = concat
    [display B0 q s, " -{", displayT q p, "}- ", display B0 q t]
  display _ q (Path (K _)) = "."
  display _ q (Path (R x t)) = concat ["\\ ", y, " -> ", display B1 (glomP q y) t]
    where y = freshen q (nom x)
  display _ q (KanT k) = displayK q k
  display _ q (Inter i) = displayI q i
  display _ q (s ::: t) = display B0 q s ++ " : " ++ display B1 q t
  display _ q (f :$ s) = display B1 q f ++ " " ++ display B0 q s
  display _ q (f :. s) = display B1 q f ++ " " ++ display B0 q s
  display _ q (f :@ b) = display B1 q f ++ " " ++ show b
  display _ q (r :^ t) = concat [display B1 q r, " {", displayT q t, "}"]
  display _ q (KanV du k v) = concat
    [displayK q k, case du of {B0 -> "\\/ "; B1 -> "/\\ "}, display B1 q v]
  display _ q (InterV du i v) = concat
    [displayI q i, case du of {B0 -> "\\/ "; B1 -> "/\\ "}, display B1 q v]
  
  displayT :: QJ g -> Triple (Syn g TM) -> String
  displayT q (Tr _ (Path (K t)) _) = "\\ _ -> " ++ display B1 q t
  displayT q (Tr _ st _) = display B1 q st
  
  qproj :: QJ g -> Var g b -> FV b
  qproj (_ :\\ v) V0 = v
  qproj (q :\\ _) (VS i) = qproj q i
  
  displayK :: QJ g -> KAN (Syn g) -> String
  displayK q (KAN s0 s1 b v h) = concat
    [ "[", displayT q s0, " | ", display B1 q b, " | ", displayT q s1, "]("
    , display B1 q v, ", ", display B1 q h, ")"]
  
  displayP :: QJ g -> Pair (Syn g TM) -> String
  displayP q (Pr a b) = display B1 q a ++ " <-> " ++ display B1 q b
  
  displayI :: QJ g -> INTERPOL (Syn g) -> String
  displayI q (INTERPOL st fg pq hk i) = concat
    [ "[", displayP q st, " | ", displayP q fg, " | ", displayP q pq
    , " | ", displayP q hk, "](" , display B1 q i, ")"]
  
  nameUsed :: QJ g -> String -> Bool
  nameUsed Q0 _ = False
  nameUsed (q :\\ Par _ _ (Nom x)) y = x == y || nameUsed q y
  nameUsed (q :\\ Dim _ (Nom x)) y = x == y || nameUsed q y
  
  freshen :: QJ g -> String -> String
  freshen q x = if nameUsed q x then go 0 else x where
    go i = if nameUsed q xi then go (i + 1) else xi where
      xi = x ++ show i
  
  glomE :: QJ g -> String -> QJ (g :\ EL)
  glomE q x = q :\\ Par 0 VType (Nom x)  -- yuk
  
  glomP :: QJ g -> String -> QJ (g :\ PT)
  glomP q x = q :\\ Dim 0 (Nom x)  -- yuk
  
  data Expt
    = (String, Syn C0 TM) :/ (FV EL -> Expt)
    | Go (Syn C0 EL)
  
  instance Show Expt where
    show e = go e 0 where
      go (Go e) i = concat
        [ "----------------------\n"
        , display B1 Q0 e
        , "\n  -->\n"
        , display B1 Q0 (t ::: tT)
        ] where
        (vt, vT) = eval E0 e i
        tT = quote Q0 VType vT i
        t  = quote Q0 vT vt i
      go ((x, s) :/ e) i = concat
        [ x, " : ", display B1 Q0 s, "\n"
        , go (e (Par i (eval E0 s i) (Nom x))) (i + 1)
        ]
  
  expt0 :: Expt
  expt0 =
    ("X", Type) :/ \ xX -> ("Y", Type) :/ \ yY ->
    ("f", B Pi (E (P xX)) (K (E (P yY)))) :/ \ f ->
    ("X'", Type) :/ \ xX' -> ("Y'", Type) :/ \ yY' ->
    ("XQ", E (P xX) :-: E (P xX')) :/ \ xXQ ->
    ("YQ", E (P yY) :-: E (P yY')) :/ \ yYQ ->
    Go
     (E (P f) :^ Tr (B Pi (E (P xX)) (K (E (P yY))))
                    (Path (R (Nom "i") (B Pi (E (P xXQ :. V V0)) (K (E (P yYQ :. V V0))))))
                    (B Pi (E (P xX')) (K (E (P yY')))))
  
  expt1 :: Expt
  expt1 =
    ("X", Type) :/ \ xX -> ("Y", Type) :/ \ yY ->
    ("XY", E (P xX) :-: E (P yY)) :/ \ qXY ->
    ("x", E (P xX)) :/ \ x ->
    Go $ Path (R (Nom "i") (E (E (P x) :^
               Tr (E (P xX))
                  (Path (R (Nom "j") (E (P qXY :. Mux (V V0) (I B0) (V (VS V0))))))
                  (E (P qXY :. V V0)))))
         :::
         Conn (E (P x))
              (Tr (E (P xX)) (E (P qXY)) (E (P yY)))
              (E (E (P x) :^ Tr (E (P xX)) (E (P qXY)) (E (P yY))))
  