{-# OPTIONS --without-K #-}

-- The two-sorted Mixed-Context Type Theory (MCTT), defined by induction-induction

module mctt where

-- First we declare the types and type families

data Cxt : Set                  -- Mixed kind/type contexts

data Kind : Cxt  Set           -- Kinds in context

data Ty : Cxt  Set             -- Types in context

data Sub : Cxt  Cxt  Set  -- Explicit substitutions between contexts

data Tm : (cxt : Cxt)  Kind cxt  Set -- Terms in kinds

--- There is no need for elements of types
--data TTm : (cxt : Cxt) → Ty cxt → Set

data _≣_ : {cxt : Cxt}  Kind cxt  Kind cxt  Set -- Judgmental equality for kinds

data _≡_ : {cxt : Cxt}  Ty cxt  Ty cxt  Set -- Judgmental equality for types

data _≗_ : {cxt : Cxt}  {k : Kind cxt}  Tm cxt k  Tm cxt k  Set -- Judgmental equality for terms

-- Now we give their constructors

-- A context is either empty, or obtained by extending another
-- context by a type variable or a kind variable.
data Cxt where
  ε : Cxt
  _,_ : (cxt : Cxt)  (t : Ty cxt)  Cxt
  _,,_ : (cxt : Cxt)  (k : Kind cxt)  Cxt

infixl 8 _,_ _,,_

-- A kind is either the universe, or a dependent product of a kind
-- over a type, or obtained by substitution from another kind.
data Kind where
  U : {cxt : Cxt}  Kind cxt
  Π : {cxt : Cxt}  (t : Ty cxt)  (k : Kind (cxt , t))  Kind cxt
  _[_] : {cxt1 cxt2 : Cxt}  (k : Kind cxt2)  (f : Sub cxt1 cxt2)  Kind cxt1

-- A type is either
data Ty where
  -- the elements of a term in the universe
  el : {cxt : Cxt}  (x : Tm cxt U)  Ty cxt
  -- obtained by substitution from another type.
  _[_] : {cxt1 cxt2 : Cxt}  (t : Ty cxt2)  (f : Sub cxt1 cxt2)  Ty cxt1

-- A substitution is either
data Sub where
  -- the identity
  id : {cxt : Cxt}  Sub cxt cxt
  -- the composite of substitutions
  _∘_ : {cxt1 cxt2 cxt3 : Cxt}  (g : Sub cxt2 cxt3)  (f : Sub cxt1 cxt2)  Sub cxt1 cxt3
  -- the projection away of a kind
  kpop : {cxt : Cxt}  (k : Kind cxt)  Sub (cxt ,, k) cxt
  -- the projection away of a type
  tpop : {cxt : Cxt}  (t : Ty cxt)  Sub (cxt , t) cxt
  -- an extension af a substitution by a term in a kind
  _≪_ : {cxt1 cxt2 : Cxt}  {k : Kind cxt2}  (f : Sub cxt1 cxt2)  Tm cxt1 (k [ f ])  Sub cxt1 (cxt2 ,, k)
  --- (Since there are no terms belonging to types, there is no _<_
  ---  extending by a term in a type.)
  -- an extension of the identity by a judgmental equality between kinds
  _id≪≣_ : (cxt : Cxt)  {k1 : Kind cxt}  {k2 : Kind cxt}  (k1  k2)  Sub (cxt ,, k1) (cxt ,, k2)
  -- Similarly, an extension of the identity by a judgmental equality between types
  _id<≡_ : (cxt : Cxt)  {t1 : Ty cxt}  {t2 : Ty cxt}  (t1  t2)  Sub (cxt , t1) (cxt , t2)
  --- (Because we lack _<_, we include also:)
  -- an extension of a substitution by the identity on a type.  This is Chapman's ↗.
  _<id_ : {cxt1 cxt2 : Cxt}  (f : Sub cxt1 cxt2)  (t : Ty cxt2)  Sub (cxt1 , t [ f ]) (cxt2 , t)
  --- (Both id<≡ and <id are definable in terms of
  ----   _<≡_ : {cxt1 cxt2 : Cxt} → (f : Sub cxt1 cxt2) → {t1 : Ty cxt1} → {t2 : Ty cxt2} → (t1 ≡ t2 [ f ]) → Sub (cxt1 , t1) (cxt2 , t2)
  ---   but we include them separately to avoid the need for
  ---   induction-recursion types.  Conversely, <≡ is definable as a
  ---   composite of <id and id<≡; see below.  Finally, the analogous
  ---   ≪id and ≪≣ are also defined below in terms of ≪ and id≪≣.)

-- A term is either
data Tm where
  -- the last kind variable
  ktop : {cxt : Cxt}  {k : Kind cxt}  Tm (cxt ,, k) (k [ kpop k ])
  -- obtained by substitution from another term
  _[_] : {cxt1 cxt2 : Cxt}  {k : Kind cxt2}  Tm cxt2 k  (f : Sub cxt1 cxt2)  Tm cxt1 (k [ f ])
  -- the application of a dependent product term
  ap : {cxt : Cxt}  {t : Ty cxt}  {k : Kind (cxt , t)}  Tm cxt (Π t k)  Tm (cxt , t) k
  -- or coercion along a judgmental equality
  coe : {cxt : Cxt}  {k1 k2 : Kind cxt}  (k1  k2)  Tm cxt k1  Tm cxt k2

-- A judgmental equality between kinds is either
data _≣_ where
  -- groupoid structure
  refl≣ : {cxt : Cxt}  (k : Kind cxt)  (k  k)
  _•_ : {cxt : Cxt}  {k1 k2 k3 : Kind cxt}  (k2  k3)  (k1  k2)  (k1  k3)
  _⁻¹ : {cxt : Cxt}  {k1 k2 : Kind cxt}  (k1  k2)  (k2  k1)
  -- functoriality of substitution
  k[id] : {cxt : Cxt}  (k : Kind cxt)  (k  k [ id ]) -- Chapman's rid
  k[∘] : {cxt1 cxt2 cxt3 : Cxt}  (k : Kind cxt3)  (f2 : Sub cxt2 cxt3)  (f1 : Sub cxt1 cxt2)  
    k [ f2 ] [ f1 ]  k [ f2  f1 ] -- Chapman's assoc
  -- a substitution of the universe equals the universe
  U[] : {cxt1 cxt2 : Cxt}  (f : Sub cxt1 cxt2)  U [ f ]  U
  -- a substitution of a dependent product equals a dependent product
  Π[] : {cxt1 cxt2 : Cxt}  (t : Ty cxt2)  (k : Kind (cxt2 , t))  (f : Sub cxt1 cxt2) 
    (Π t k) [ f ]  (Π (t [ f ]) (k [ f <id t ])) -- (k [ f <≡ refl≡ (t [ f ]) ]))
  -- congruence of Π.  Arguably there should be a (t ≡ t') as well, but that's tricky to type and we haven't needed it yet.
  Π≣ : {cxt : Cxt}  (t : Ty cxt)  {k k' : Kind (cxt , t)}  (k  k')  (Π t k  Π t k')
  -- congruence of ≣
  _[_] : {cxt1 cxt2 : Cxt}  {k1 k2 : Kind cxt2}  (k1  k2)  (f : Sub cxt1 cxt2)  (k1 [ f ]  k2 [ f ])
  -- a commutation of kpop and tpop (should really be a judgmental equality of substitutions)
  ktpop≣ : {cxt : Cxt}  (h k : Kind cxt)  (t : Ty cxt)  
    h [ kpop k ] [ tpop (t [ kpop k ]) ]   h [ tpop t ] [ kpop k <id t ] --  [ kpop k <≡ refl≡ (t [ kpop k ]) ]
  -- whatever this is (also an equality of substitutions)
  kpop∘≪ : {cxt1 cxt2 : Cxt} {k : Kind cxt2} (f : Sub cxt1 cxt2) (x : Tm cxt1 (k [ f ])) 
    k [ f ]  (k [ kpop k ]) [ f  x ]

-- A judgmental equality between types is either
data _≡_ where
  -- groupoid structure
  refl≡ : {cxt : Cxt}  (t : Ty cxt)  (t  t)
  _•_ : {cxt : Cxt}  {t1 t2 t3 : Ty cxt}  (t2  t3)  (t1  t2)  (t1  t3)
  _⁻¹ : {cxt : Cxt}  {t1 t2 : Ty cxt}  (t1  t2)  (t2  t1)
  -- functoriality of substitution
  t[id] : {cxt : Cxt}  (t : Ty cxt)  (t  t [ id ]) -- Chapman's rid
  t[∘] : {cxt1 cxt2 cxt3 : Cxt}  (t : Ty cxt3)  (f2 : Sub cxt2 cxt3)  (f1 : Sub cxt1 cxt2) 
    t [ f2 ] [ f1 ]  t [ f2  f1 ] -- Chapman's assoc
  -- a substitution of el equals an el
  el[] : {cxt1 cxt2 : Cxt}  (x : Tm cxt2 U)  (f : Sub cxt1 cxt2)  (el x [ f ]  el (coe (U[] f) (x [ f ])))
  -- congruence of el
  --- el≡ : something involving ≗
  -- congruence of ≡
  _[_] : {cxt1 cxt2 : Cxt}  {t1 t2 : Ty cxt2}  (t1  t2)  (f : Sub cxt1 cxt2)  (t1 [ f ]  t2 [ f ])
  -- a commutation of kpop and tpop (should really be a judgmental equality of substitutions)
  ktpop≡ : {cxt : Cxt}  (s : Ty cxt)  (k : Kind cxt)  (t : Ty cxt)  
    s [ kpop k ] [ tpop (t [ kpop k ]) ]  s [ tpop t ] [ kpop k <id t ]

data _≗_ where
  -- groupoid structure
  refl≗ : {cxt : Cxt}  {k : Kind cxt}  (x : Tm cxt k)  (x  x)
  _•_ : {cxt : Cxt}  {k : Kind cxt}  {x1 x2 x3 : Tm cxt k}  (x2  x3)  (x1  x2)  (x1  x3)
  _⁻¹ : {cxt : Cxt}  {k : Kind cxt}  {x1 x2 : Tm cxt k}  (x1  x2)  (x2  x1)
  -- functoriality of coercion
  coe-id : {cxt : Cxt}  {k : Kind cxt}  (x : Tm cxt k)  coe (refl≣ k) x  x
  coe• : {cxt : Cxt}  {k1 k2 k3 : Kind cxt}  (x : Tm cxt k1)  (e2 : k2  k3)  (e1 : k1  k2) 
    coe e2 (coe e1 x)  coe (e2  e1) x
  -- substitution of coercion
  coe[] : {cxt1 cxt2 : Cxt}  {k1 k2 : Kind cxt2}  (eq : k1  k2)  (x : Tm cxt2 k1)  (f : Sub cxt1 cxt2) 
    coe eq x [ f ]  coe (eq [ f ]) (x [ f ])
  -- umm, what do I call this except what it is?
  ktop≪ : {cxt1 cxt2 : Cxt}  {k : Kind cxt2}  (f : Sub cxt1 cxt2)  (x : Tm cxt1 (k [ f ])) 
    ktop [ f  x ]  coe (kpop∘≪ f x) x

------------------------------
-- Auxiliary functions
------------------------------

-- For reference, here are the possible definitions of <id and id<≡ in terms of <≡.

-- _<id_ : {cxt1 cxt2 : Cxt} → (f : Sub cxt1 cxt2) → (t : Ty cxt2) → Sub (cxt1 , t [ f ]) (cxt2 , t)
-- f <id t = f <≡ refl≡ (t [ f ])

--_id<≡_ : (cxt : Cxt) → {t1 : Ty cxt} → {t2 : Ty cxt} → (t1 ≡ t2) → Sub (cxt , t1) (cxt , t2)
--_id<≡_ cxt {t1} {t2} eq = (id {cxt}) <≡ (t[id] t2 • eq)

-- And now the definition of <≡ in terms of them
_<≡_ : {cxt1 cxt2 : Cxt}  (f : Sub cxt1 cxt2)  {t1 : Ty cxt1}  {t2 : Ty cxt2}  (t1  t2 [ f ])  Sub (cxt1 , t1) (cxt2 , t2)
_<≡_ {cxt1} {cxt2} f {t1} {t2} eq = (f <id t2)  (cxt1 id<≡ eq)

-- And their counterparts for kinds

-- _id≪≣_ : (cxt : Cxt) → {k1 : Kind cxt} → {k2 : Kind cxt} → (k1 ≣ k2) → Sub (cxt ,, k1) (cxt ,, k2)
-- _id≪≣_ cxt {k1} {k2} eq = (id {cxt}) ≪≣ (k[id] k2 • eq)

_≪id_ : {cxt1 cxt2 : Cxt}  (f : Sub cxt1 cxt2)  (k : Kind cxt2)  Sub (cxt1 ,, k [ f ]) (cxt2 ,, k)
f ≪id k =  (f  kpop (k [ f ]))  coe (k[∘] _ _ _) (ktop {_} {k [ f ]})

_≪≣_ : {cxt1 cxt2 : Cxt}  (f : Sub cxt1 cxt2)  {k1 : Kind cxt1}  {k2 : Kind cxt2}  (k1  k2 [ f ])  Sub (cxt1 ,, k1) (cxt2 ,, k2)
_≪≣_ f {k1} {k2} eq = (f ≪id k2)  (_ id≪≣ eq) 

-- a substitution that interchanges pops
tpop-kpop : {cxt : Cxt}  (t : Ty cxt)  (k : Kind cxt)  Sub ((cxt ,, k) , t [ kpop k ]) ((cxt , t) ,, k [ tpop t ])
tpop-kpop {cxt} t k = (kpop k <id t)  coe (ktpop≣ k k t) (ktop [ tpop (t [ kpop k ]) ])

-- a substitution that applies a Π
Πap-sub : {cxt : Cxt}  (t : Ty cxt)  (k : Kind (cxt , t))  Sub ((cxt ,, Π t k) , t [ kpop (Π t k) ]) ((cxt , t) ,, k)
Πap-sub {cxt} t k =  (kpop (Π t k) <id t)   ap (coe (Π[] t k (kpop (Π t k))) ktop)

infixl 8 _<id_  _id<≡_  _<≡_

infixl 8 _≪id_ _id≪≣_ _≪≣_

infixl 8 _≪_

infixl 8 _∘_ _•_