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

module globular where

open import Data.Nat
open import Data.Maybe
open import Data.Sum
open import Data.Product

open import mctt
open import extract

-- whether a context is all kinds, or else find the first type.

data AllKinds : Cxt → Set where
  AKε : AllKinds ε
  AK,,k : {cxt : Cxt} → AllKinds cxt → (k : Kind cxt) → AllKinds (cxt ,, k)

data FirstTy : Cxt → Set where
  FT,t₁ : {cxt : Cxt} → AllKinds cxt → (t : Ty cxt) → FirstTy (cxt , t)
  FT,t₊ : {cxt : Cxt} → FirstTy cxt → (t : Ty cxt) → FirstTy (cxt , t)
  FT,,k : {cxt : Cxt} → FirstTy cxt → (k : Kind cxt) → FirstTy (cxt ,, k)

AK⊎FT : (cxt : Cxt) → AllKinds cxt ⊎ FirstTy cxt
AK⊎FT ε = inj₁ AKε
AK⊎FT (cxt , t) = helper (AK⊎FT cxt) where
  helper : AllKinds cxt ⊎ FirstTy cxt → AllKinds (cxt , t) ⊎ FirstTy (cxt , t)
  helper (inj₁ ak) = inj₂ (FT,t₁ ak t)
  helper (inj₂ ft) = inj₂ (FT,t₊ ft t)
AK⊎FT (cxt ,, k) =  helper (AK⊎FT cxt) where
  helper : AllKinds cxt ⊎ FirstTy cxt → AllKinds (cxt ,, k) ⊎ FirstTy (cxt ,, k)
  helper (inj₁ ak) = inj₁ (AK,,k ak k)
  helper (inj₂ ft) = inj₂ (FT,,k ft k)

----------------------------------------
-- Extending by a single type variable with two inhabitants
----------------------------------------

-- Insert a new kind variable X:U at the beginning, and two new type
-- variables x₁:X, x₂:X just before the first existing type variable (or at
-- the end, if there are none).  Furthermore, all kind variables
-- occurring in between are made indexed over X.
gcxt : Cxt → Cxt

-- Helper function for tcxt.
gcxt? : (cxt : Cxt) → AllKinds cxt ⊎ FirstTy cxt → Cxt

-- gcxt is easy to define in terms of its helper function.
gcxt cxt = gcxt? cxt (AK⊎FT cxt)

-- Given a context consisting of all kinds, do as gcxt but omit x₁,x₂ at
-- the end.
gcxt-ak : (cxt : Cxt) → AllKinds cxt → Cxt

-- The types of the variables x₁,x₂:X to be added to gcxt-ak
gnewty₁-ak : (cxt : Cxt) → (ak : AllKinds cxt) → Ty (gcxt-ak cxt ak)
gnewty₂-ak : (cxt : Cxt) → (ak : AllKinds cxt) → Ty (gcxt-ak cxt ak , gnewty₁-ak cxt ak)

-- Given a context *not* consisting of all kinds, do as gcxt.
gcxt-ft : (cxt : Cxt) → FirstTy cxt → Cxt

-- Now gcxt? is easy to define in terms of its helper functions.
gcxt? cxt (inj₁ ak) =  ((gcxt-ak cxt ak , gnewty₁-ak cxt ak) , gnewty₂-ak cxt ak)
gcxt? cxt (inj₂ ft) =  (gcxt-ft cxt ft)

-- Given a kind in context, find the same kind in the extended context.
gkind : {cxt : Cxt} → (k : Kind cxt) → Kind (gcxt cxt)

-- Helper function for tkind
gkind? : {cxt : Cxt} → (akft : AllKinds cxt ⊎ FirstTy cxt) → (k : Kind cxt) → Kind (gcxt? cxt akft)

-- tkind is easy to define in terms of its helper function.
gkind {cxt} k = gkind? (AK⊎FT cxt) k

-- Same for a type in context
gty : {cxt : Cxt} → (t : Ty cxt) → Ty (gcxt cxt)
gty? : {cxt : Cxt} → (akft : AllKinds cxt ⊎ FirstTy cxt) → (t : Ty cxt) → Ty (gcxt? cxt akft)
gty {cxt} t = gty? (AK⊎FT cxt) t

-- Now gcxt-ak is defined by
gcxt-ak .ε AKε =  (ε ,, U) --  inserting X:U at the beginning, and
gcxt-ak .(cxt ,, k) (AK,,k {cxt} ak k) =
  -- indexing all new kinds over x:X.
  (gcxt-ak cxt ak ,, Π (gnewty₁-ak cxt ak) (Π (gnewty₂-ak cxt ak) (gkind? (inj₁ ak) k)))

-- For readability, we give a name to the doubly indexed kind being added
ΠΠgkind? : {cxt : Cxt} → (ak : AllKinds cxt) → Kind cxt → Kind (gcxt-ak cxt ak)
ΠΠgkind? {cxt} ak k = Π (gnewty₁-ak cxt ak) (Π (gnewty₂-ak cxt ak) (gkind? (inj₁ ak) k))

-- the types of the new variables x₁,x₂ are just X, appropriately substituted.
gnewty₁-ak .ε AKε = (el (coe (U[] (kpop U)) ktop))
gnewty₁-ak .(cxt ,, k) (AK,,k {cxt} ak k) = gnewty₁-ak cxt ak [ kpop (ΠΠgkind? ak k) ]
gnewty₂-ak cxt ak = gnewty₁-ak cxt ak [ tpop (gnewty₁-ak cxt ak) ]

-- gcxt-ft is defined by
gcxt-ft .(cxt , t) (FT,t₁ {cxt} ak t) =
  -- inserting x₁:X,x₂:X just before the first type
  (((gcxt-ak cxt ak , gnewty₁-ak cxt ak) , gnewty₂-ak cxt ak) , gty? (inj₁ ak) t)
-- and otherwise doing nothing to speak of
gcxt-ft .(cxt , t) (FT,t₊ {cxt} ft t) = (gcxt-ft cxt ft , gty? (inj₂ ft) t)
gcxt-ft .(cxt ,, k) (FT,,k {cxt} ft k) = (gcxt-ft cxt ft ,, gkind? (inj₂ ft) k)

-- A substitution from the extended context back to the original one,
-- which forgets X:U and x₁,x₂:X, while 'ap'plying all newly indexed
-- kind-variables to x₁ and x₂ to obtain values of their original kinds.
gcxt-sub? : (cxt : Cxt) → (akft : AllKinds cxt ⊎ FirstTy cxt) → Sub (gcxt? cxt akft) cxt

-- Now tkind? and tty? are easy to define by substitution.
gkind? {cxt} akft k = k [ gcxt-sub? cxt akft ]
gty? {cxt} akft t = t [ gcxt-sub? cxt akft ]

-- Finally we define this substitution.
-- When the original context is empty, we simply forget X:U and x₁,x₂:X.
gcxt-sub? .ε (inj₁ AKε) = (kpop U
                          ∘ tpop (el (coe (U[] (kpop U)) ktop)))
                          ∘ tpop (el (coe (U[] (kpop U)) ktop) [ tpop (el (coe (U[] (kpop U)) ktop)) ])
-- The nontrivial case is when we add a new kind in between X and x₁,x₂.
gcxt-sub? .(cxt ,, k) (inj₁ (AK,,k {cxt} ak k)) =
   (gcxt-sub? cxt (inj₁ ak)
    ∘ (kpop (ΠΠgkind? ak k) <id (gnewty₁-ak cxt ak) <id (gnewty₂-ak cxt ak))
    ∘ (_ id<≡ (ktpop≡ (gnewty₁-ak cxt ak) (ΠΠgkind? ak k) (gnewty₁-ak cxt ak))))
    ≪ coe (k[∘] _ _ _)
          ((coe (k[∘] _ _ _)
                (ap (coe (Π[] (gnewty₂-ak cxt ak) (k [ gcxt-sub? cxt (inj₁ ak) ])
                              (kpop (ΠΠgkind? ak k) <id gnewty₁-ak cxt ak))
                         (ap (coe (Π[] _ _ (kpop (ΠΠgkind? ak k))) ktop)))))
           [ (gcxt-ak cxt ak ,, ΠΠgkind? ak k , gnewty₁-ak cxt ak [ kpop (ΠΠgkind? ak k) ])
             id<≡ (ktpop≡ (gnewty₁-ak cxt ak) (ΠΠgkind? ak k) (gnewty₁-ak cxt ak))
           ])
-- The other three cases are easy.
gcxt-sub? .(cxt , t) (inj₂ (FT,t₁ {cxt} ak t)) = gcxt-sub? cxt (inj₁ ak) <id t
gcxt-sub? .(cxt , t) (inj₂ (FT,t₊ {cxt} ft t)) = gcxt-sub? cxt (inj₂ ft) <id t
gcxt-sub? .(cxt ,, k) (inj₂ (FT,,k {cxt} ft k)) = gcxt-sub? cxt (inj₂ ft) ≪id k

-- gcxt-ak always produces a contexts consisting only of kinds.
gcxt-ak-ak : (cxt : Cxt) → (ak : AllKinds cxt) → AllKinds (gcxt-ak cxt ak)
gcxt-ak-ak .ε AKε =  AK,,k AKε U
gcxt-ak-ak .(cxt ,, k) (AK,,k {cxt} ak k) =  AK,,k (gcxt-ak-ak cxt ak) (ΠΠgkind? ak k)

--------------------
-- Globular types
--------------------

-- By iterating gcxt (or more precisely gcxt-ak), we produce contexts
-- that represent globular types
glob : ℕ → Cxt

-- These consist only of kinds (we need that to complete the iteration).
glob-ak : (n : ℕ) → AllKinds (glob n)

glob  = ε
glob (suc n) = gcxt-ak (glob n) (glob-ak n)

glob-ak  = AKε
glob-ak (suc n) = gcxt-ak-ak (glob n) (glob-ak n)

-- Now run extract (glob 10)