System-F-iso-readback.agda

open import Level
open import Function
open import Data.Empty
open import Data.Sum.Base

infixr 6 _⇒_
infix  3 _⊢ᵗ_ _⊢ᵗⁿᵉ_ _⊢ᵗⁿᶠ_ _⊨ᵗ_ _⊢_
infixl 9 _[_]ᵗ

module Context {α} (A : Set α) where
  infixl 5 _▻_

  data Con : Set α where
    ε   : Con
    _▻_ : Con -> A -> Con

module _ where
  open Context

  mapᶜ : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> Con A -> Con B
  mapᶜ f  ε      = ε
  mapᶜ f (Γ ▻ x) = mapᶜ f Γ ▻ f x

module _ {α} {A : Set α} where
  infix 3 _⊆_ _∈_
  infixr 9 _∘ᵒ_

  open Context A

  data _⊆_ : Con -> Con -> Set where
    stop : ε ⊆ ε
    skip : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ     ⊆ Δ ▻ σ
    keep : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ ▻ σ ⊆ Δ ▻ σ

  data _∈_ σ : Con -> Set where
    vz  : ∀ {Γ}   -> σ ∈ Γ ▻ σ
    vs_ : ∀ {Γ τ} -> σ ∈ Γ     -> σ ∈ Γ ▻ τ

  idᵒ : ∀ {Γ} -> Γ ⊆ Γ
  idᵒ {ε}     = stop
  idᵒ {Γ ▻ σ} = keep idᵒ

  _∘ᵒ_ : ∀ {Γ Δ Ξ} -> Δ ⊆ Ξ -> Γ ⊆ Δ -> Γ ⊆ Ξ
  stop   ∘ᵒ ι      = ι
  skip κ ∘ᵒ ι      = skip (κ ∘ᵒ ι)
  keep κ ∘ᵒ skip ι = skip (κ ∘ᵒ ι)
  keep κ ∘ᵒ keep ι = keep (κ ∘ᵒ ι)

  top : ∀ {Γ σ} -> Γ ⊆ Γ ▻ σ
  top = skip idᵒ

  renᵛ : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> σ ∈ Γ -> σ ∈ Δ
  renᵛ  stop     ()
  renᵛ (skip ι)  v     = vs (renᵛ ι v)
  renᵛ (keep ι)  vz    = vz
  renᵛ (keep ι) (vs v) = vs (renᵛ ι v)

  record Environment {β} (_∙_ : Con -> A -> Set β) : Set (α ⊔ β) where
    infix 3 _⊢ᵉ_

    field
      renᶠ   : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ ∙ σ -> Δ ∙ σ
      freshᶠ : ∀ {Γ σ} -> (Γ ▻ σ) ∙ σ

    data _⊢ᵉ_ Δ : Con -> Set β where
      Ø   : Δ ⊢ᵉ ε
      _▷_ : ∀ {Γ σ} -> Δ ⊢ᵉ Γ -> Δ ∙ σ -> Δ ⊢ᵉ Γ ▻ σ

    lookupᵉ : ∀ {Δ Γ σ} -> σ ∈ Γ -> Δ ⊢ᵉ Γ -> Δ ∙ σ
    lookupᵉ  vz    (ρ ▷ t) = t
    lookupᵉ (vs v) (ρ ▷ t) = lookupᵉ v ρ

    renᵉ : ∀ {Δ Ξ Γ} -> Δ ⊆ Ξ -> Δ ⊢ᵉ Γ -> Ξ ⊢ᵉ Γ
    renᵉ ι  Ø      = Ø
    renᵉ ι (ρ ▷ t) = renᵉ ι ρ ▷ renᶠ ι t

    keepᵉ : ∀ {Δ Γ σ} -> Δ ⊢ᵉ Γ -> Δ ▻ σ ⊢ᵉ Γ ▻ σ
    keepᵉ ρ = renᵉ top ρ ▷ freshᶠ

    idᵉ : ∀ {Γ} -> Γ ⊢ᵉ Γ
    idᵉ {ε}     = Ø
    idᵉ {Γ ▻ σ} = keepᵉ idᵉ

    topᵉ : ∀ {Γ σ} -> Γ ∙ σ -> Γ ⊢ᵉ Γ ▻ σ
    topᵉ t = idᵉ ▷ t

data Kind : Set where
  ⋆    : Kind
  _⇒ᵏ_ : Kind -> Kind -> Kind

open Context Kind renaming (Con to Conᵏ; ε to εᵏ; _▻_ to _▻ᵏ_)

mutual
  Type : Conᵏ -> Set
  Type Θ = Θ ⊢ᵗ ⋆

  data _⊢ᵗ_ Θ : Kind -> Set where
    Var : ∀ {σ} -> σ ∈ Θ -> Θ ⊢ᵗ σ
    Lam : ∀ {σ τ} -> Θ ▻ᵏ σ ⊢ᵗ τ -> Θ ⊢ᵗ σ ⇒ᵏ τ
    App  : ∀ {σ τ} -> Θ ⊢ᵗ σ ⇒ᵏ τ -> Θ ⊢ᵗ σ -> Θ ⊢ᵗ τ
    _⇒_  : Type Θ -> Type Θ -> Type Θ
    π    : ∀ σ -> Type (Θ ▻ᵏ σ) -> Type Θ
    Fix : Type (Θ ▻ᵏ ⋆) -> Type Θ

renᵗ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢ᵗ σ -> Ξ ⊢ᵗ σ
renᵗ ι (Var v)   = Var (renᵛ ι v)
renᵗ ι (Lam β)   = Lam (renᵗ (keep ι) β)
renᵗ ι (App ψ α) = App (renᵗ ι ψ) (renᵗ ι α)
renᵗ ι (α ⇒ β)   = renᵗ ι α ⇒ renᵗ ι β
renᵗ ι (π σ α)   = π σ (renᵗ (keep ι) α)
renᵗ ι (Fix ψ)   = Fix (renᵗ (keep ι) ψ)

shiftᵗ : ∀ {Θ σ τ} -> Θ ⊢ᵗ σ -> Θ ▻ᵏ τ ⊢ᵗ σ
shiftᵗ = renᵗ top

open module TypeCon Θ = Context (Type Θ)

shiftᶜ : ∀ {Θ σ} -> Con Θ -> Con (Θ ▻ᵏ σ)
shiftᶜ = mapᶜ shiftᵗ

mutual
  Typeⁿᵉ : Conᵏ -> Set
  Typeⁿᵉ Θ = Θ ⊢ᵗⁿᵉ ⋆

  Typeⁿᶠ : Conᵏ -> Set
  Typeⁿᶠ Θ = Θ ⊢ᵗⁿᶠ ⋆

  data _⊢ᵗⁿᵉ_ Θ : Kind -> Set where
    Varⁿᵉ : ∀ {σ} -> σ ∈ Θ -> Θ ⊢ᵗⁿᵉ σ
    Appⁿᵉ : ∀ {σ τ} -> Θ ⊢ᵗⁿᵉ σ ⇒ᵏ τ -> Θ ⊢ᵗⁿᶠ σ -> Θ ⊢ᵗⁿᵉ τ
    _⇒ⁿᵉ_ : Typeⁿᵉ Θ -> Typeⁿᵉ Θ -> Typeⁿᵉ Θ
    πⁿᵉ   : ∀ σ -> Typeⁿᵉ (Θ ▻ᵏ σ) -> Typeⁿᵉ Θ
    Fixⁿᵉ : Typeⁿᵉ (Θ ▻ᵏ ⋆) -> Typeⁿᵉ Θ

  data _⊢ᵗⁿᶠ_ Θ : Kind -> Set where
    Neⁿᶠ   : ∀ {σ} -> Θ ⊢ᵗⁿᵉ σ -> Θ ⊢ᵗⁿᶠ σ
    Lamⁿᶠ_ : ∀ {σ τ} -> Θ ▻ᵏ σ ⊢ᵗⁿᶠ τ -> Θ ⊢ᵗⁿᶠ σ ⇒ᵏ τ

mutual
  embᵗⁿᵉ : ∀ {Θ σ} -> Θ ⊢ᵗⁿᵉ σ -> Θ ⊢ᵗ σ
  embᵗⁿᵉ (Varⁿᵉ v)   = Var v
  embᵗⁿᵉ (Appⁿᵉ ψ α) = App (embᵗⁿᵉ ψ) (embᵗⁿᶠ α)
  embᵗⁿᵉ (α ⇒ⁿᵉ β)   = embᵗⁿᵉ α ⇒ embᵗⁿᵉ β
  embᵗⁿᵉ (πⁿᵉ σ α)   = π σ (embᵗⁿᵉ α)
  embᵗⁿᵉ (Fixⁿᵉ ψ)   = Fix (embᵗⁿᵉ ψ)

  embᵗⁿᶠ : ∀ {Θ σ} -> Θ ⊢ᵗⁿᶠ σ -> Θ ⊢ᵗ σ
  embᵗⁿᶠ (Neⁿᶠ α)  = embᵗⁿᵉ α
  embᵗⁿᶠ (Lamⁿᶠ β) = Lam (embᵗⁿᶠ β)

mutual
  renᵗⁿᵉ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢ᵗⁿᵉ σ -> Ξ ⊢ᵗⁿᵉ σ
  renᵗⁿᵉ ι (Varⁿᵉ v)   = Varⁿᵉ (renᵛ ι v)
  renᵗⁿᵉ ι (Appⁿᵉ ψ α) = Appⁿᵉ (renᵗⁿᵉ ι ψ) (renᵗⁿᶠ ι α)
  renᵗⁿᵉ ι (α ⇒ⁿᵉ β)   = renᵗⁿᵉ ι α ⇒ⁿᵉ renᵗⁿᵉ ι β
  renᵗⁿᵉ ι (πⁿᵉ σ α)   = πⁿᵉ σ (renᵗⁿᵉ (keep ι) α)
  renᵗⁿᵉ ι (Fixⁿᵉ ψ)   = Fixⁿᵉ (renᵗⁿᵉ (keep ι) ψ)

  renᵗⁿᶠ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢ᵗⁿᶠ σ -> Ξ ⊢ᵗⁿᶠ σ
  renᵗⁿᶠ ι (Neⁿᶠ α)  = Neⁿᶠ (renᵗⁿᵉ ι α)
  renᵗⁿᶠ ι (Lamⁿᶠ β) = Lamⁿᶠ (renᵗⁿᶠ (keep ι) β)

mutual
  _⊨ᵗ_ : Conᵏ -> Kind -> Set
  Θ ⊨ᵗ σ = Θ ⊢ᵗⁿᵉ σ ⊎ Kripke Θ σ

  Kripke : Conᵏ -> Kind -> Set
  Kripke Θ  ⋆       = ⊥
  Kripke Θ (σ ⇒ᵏ τ) = ∀ {Ξ} -> Θ ⊆ Ξ -> Ξ ⊨ᵗ σ -> Ξ ⊨ᵗ τ

Neˢ : ∀ {σ Θ} -> Θ ⊢ᵗⁿᵉ σ -> Θ ⊨ᵗ σ
Neˢ = inj₁

Varˢ : ∀ {σ Θ} -> σ ∈ Θ -> Θ ⊨ᵗ σ
Varˢ = Neˢ ∘ Varⁿᵉ

renᵗˢ : ∀ {σ Θ Δ} -> Θ ⊆ Δ -> Θ ⊨ᵗ σ -> Δ ⊨ᵗ σ
renᵗˢ          ι  (inj₁ α)  = inj₁ (renᵗⁿᵉ ι α)
renᵗˢ {⋆}      ι  (inj₂ ())
renᵗˢ {σ ⇒ᵏ τ} ι (inj₂ k)  = inj₂ λ κ -> k (κ ∘ᵒ ι)

readbackᵗ : ∀ {σ Θ} -> Θ ⊨ᵗ σ -> Θ ⊢ᵗⁿᶠ σ
readbackᵗ           (inj₁ α)  = Neⁿᶠ α
readbackᵗ {⋆}       (inj₂ ())
readbackᵗ {σ ⇒ᵏ τ} (inj₂ k)  = Lamⁿᶠ (readbackᵗ (k top (Varˢ vz)))

Appˢ : ∀ {Θ σ τ} -> Θ ⊨ᵗ σ ⇒ᵏ τ -> Θ ⊨ᵗ σ -> Θ ⊨ᵗ τ
Appˢ (inj₁ f) x = Neˢ (Appⁿᵉ f (readbackᵗ x))
Appˢ (inj₂ k) x = k idᵒ x

groundⁿᵉ : ∀ {Θ} -> Θ ⊨ᵗ ⋆ -> Θ ⊢ᵗⁿᵉ ⋆
groundⁿᵉ (inj₁ α)  = α
groundⁿᵉ (inj₂ ())

environmentᵗˢ : Environment _⊨ᵗ_
environmentᵗˢ = record
  { renᶠ   = renᵗˢ
  ; freshᶠ = Varˢ vz
  }

module _ where
  open Environment environmentᵗˢ

  ⟦_⟧ᵗ : ∀ {Θ Ξ σ} -> Θ ⊢ᵗ σ -> Ξ ⊢ᵉ Θ -> Ξ ⊨ᵗ σ
  ⟦ Var v   ⟧ᵗ ρ = lookupᵉ v ρ
  ⟦ Lam β   ⟧ᵗ ρ = inj₂ λ ι α -> ⟦ β ⟧ᵗ (renᵉ ι ρ ▷ α)
  ⟦ App ψ α ⟧ᵗ ρ = Appˢ (⟦ ψ ⟧ᵗ ρ) (⟦ α ⟧ᵗ ρ)
  ⟦ α ⇒ β   ⟧ᵗ ρ = inj₁ (groundⁿᵉ (⟦ α ⟧ᵗ ρ) ⇒ⁿᵉ groundⁿᵉ (⟦ β ⟧ᵗ ρ))
  ⟦ π σ α   ⟧ᵗ ρ = inj₁ (πⁿᵉ σ (groundⁿᵉ (⟦ α ⟧ᵗ (keepᵉ ρ))))
  ⟦ Fix ψ   ⟧ᵗ ρ = inj₁ (Fixⁿᵉ (groundⁿᵉ (⟦ ψ ⟧ᵗ (keepᵉ ρ))))

  evalᵗ : ∀ {Θ σ} -> Θ ⊢ᵗ σ -> Θ ⊨ᵗ σ
  evalᵗ α = ⟦ α ⟧ᵗ idᵉ

nfᵗ : ∀ {Θ σ} -> Θ ⊢ᵗ σ -> Θ ⊢ᵗⁿᶠ σ
nfᵗ = readbackᵗ ∘ evalᵗ

normalize : ∀ {Θ σ} -> Θ ⊢ᵗ σ -> Θ ⊢ᵗ σ
normalize = embᵗⁿᶠ ∘ nfᵗ

_[_]ᵗ : ∀ {Θ σ τ} -> Θ ▻ᵏ σ ⊢ᵗ τ -> Θ ⊢ᵗ σ -> Θ ⊢ᵗ τ
β [ α ]ᵗ = normalize (App (Lam β) α)

data _⊢_ {Θ} Γ : Type Θ -> Set where
  var  : ∀ {α}   -> α ∈ Γ -> Γ ⊢ α
  Λ_   : ∀ {σ α} -> shiftᶜ Γ ⊢ α -> Γ ⊢ π σ α
  _[_] : ∀ {σ β} -> Γ ⊢ π σ β -> (α : Θ ⊢ᵗ σ) -> Γ ⊢ β [ α ]ᵗ
  ƛ_   : ∀ {α β} -> Γ ▻ α ⊢ β -> Γ ⊢ α ⇒ β
  _·_  : ∀ {α β} -> Γ ⊢ α ⇒ β -> Γ ⊢ α -> Γ ⊢ β
  wrap   : ∀ {ψ} -> Γ ⊢ ψ [ Fix ψ ]ᵗ -> Γ ⊢ Fix ψ
  unwrap : ∀ {ψ} -> Γ ⊢ Fix ψ -> Γ ⊢ ψ [ Fix ψ ]ᵗ
  

System-F-iso.agda

open import Level

infixr 6 _⇒_
infix  3 _⊢∙ᵗ_ _⊢ᵗ_ _⊢⋆ᵗ_ _⊢_
infixl 9 _[_]ᵗ

module Context {α} (A : Set α) where
  infixl 5 _▻_

  data Con : Set α where
    ε   : Con
    _▻_ : Con -> A -> Con

module _ where
  open Context

  mapᶜ : ∀ {α β} {A : Set α} {B : Set β} -> (A -> B) -> Con A -> Con B
  mapᶜ f  ε      = ε
  mapᶜ f (Γ ▻ x) = mapᶜ f Γ ▻ f x

module _ {α} {A : Set α} where
  infix 3 _⊆_ _∈_

  open Context A

  data _⊆_ : Con -> Con -> Set where
    stop : ε ⊆ ε
    skip : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ     ⊆ Δ ▻ σ
    keep : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ ▻ σ ⊆ Δ ▻ σ

  data _∈_ σ : Con -> Set where
    vz  : ∀ {Γ}   -> σ ∈ Γ ▻ σ
    vs_ : ∀ {Γ τ} -> σ ∈ Γ     -> σ ∈ Γ ▻ τ

  id : ∀ {Γ} -> Γ ⊆ Γ
  id {ε}     = stop
  id {Γ ▻ σ} = keep id

  top : ∀ {Γ σ} -> Γ ⊆ Γ ▻ σ
  top = skip id

  renᵛ : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> σ ∈ Γ -> σ ∈ Δ
  renᵛ  stop     ()
  renᵛ (skip ι)  v     = vs (renᵛ ι v)
  renᵛ (keep ι)  vz    = vz
  renᵛ (keep ι) (vs v) = vs (renᵛ ι v)

  record Environment {β} (_∙_ : Con -> A -> Set β) : Set (α ⊔ β) where
    infix 3 _⊢ᵉ_

    field
      renᶠ   : ∀ {Γ Δ σ} -> Γ ⊆ Δ -> Γ ∙ σ -> Δ ∙ σ
      freshᶠ : ∀ {Γ σ} -> (Γ ▻ σ) ∙ σ

    data _⊢ᵉ_ Δ : Con -> Set β where
      Ø   : Δ ⊢ᵉ ε
      _▷_ : ∀ {Γ σ} -> Δ ⊢ᵉ Γ -> Δ ∙ σ -> Δ ⊢ᵉ Γ ▻ σ

    lookupᵉ : ∀ {Δ Γ σ} -> σ ∈ Γ -> Δ ⊢ᵉ Γ -> Δ ∙ σ
    lookupᵉ  vz    (ρ ▷ t) = t
    lookupᵉ (vs v) (ρ ▷ t) = lookupᵉ v ρ

    renᵉ : ∀ {Δ Ξ Γ} -> Δ ⊆ Ξ -> Δ ⊢ᵉ Γ -> Ξ ⊢ᵉ Γ
    renᵉ ι  Ø      = Ø
    renᵉ ι (ρ ▷ t) = renᵉ ι ρ ▷ renᶠ ι t

    keepᵉ : ∀ {Δ Γ σ} -> Δ ⊢ᵉ Γ -> Δ ▻ σ ⊢ᵉ Γ ▻ σ
    keepᵉ ρ = renᵉ top ρ ▷ freshᶠ

    idᵉ : ∀ {Γ} -> Γ ⊢ᵉ Γ
    idᵉ {ε}     = Ø
    idᵉ {Γ ▻ σ} = keepᵉ idᵉ

    topᵉ : ∀ {Γ σ} -> Γ ∙ σ -> Γ ⊢ᵉ Γ ▻ σ
    topᵉ t = idᵉ ▷ t

data Kind : Set where
  ⋆    : Kind
  _⇒ᵏ_ : Kind -> Kind -> Kind

open Context Kind renaming (Con to Conᵏ; ε to εᵏ; _▻_ to _▻ᵏ_)

mutual
  Type : Conᵏ -> Set
  Type Θ = Θ ⊢ᵗ ⋆

  -- A head of an application. In usual hereditary substitution the only thing that can be a head
  -- is a variable, we also allow `Fix`.
  data _⊢∙ᵗ_ Θ : Kind -> Set where
    Var : ∀ {σ} -> σ ∈ Θ -> Θ ⊢∙ᵗ σ
    Fix : ∀ {σ} -> Θ ▻ᵏ σ ⊢ᵗ σ -> Θ ⊢∙ᵗ σ

  -- A type defined in a kind context.
  data _⊢ᵗ_ Θ : Kind -> Set where
    Lam  : ∀ {σ τ} -> Θ ▻ᵏ σ ⊢ᵗ τ -> Θ ⊢ᵗ σ ⇒ᵏ τ
    App  : ∀ {σ} -> Θ ⊢∙ᵗ σ -> Θ ⊢⋆ᵗ σ -> Type Θ
    _⇒_  : Type Θ -> Type Θ -> Type Θ
    π    : ∀ σ -> Type (Θ ▻ᵏ σ) -> Type Θ

  -- A spine.
  data _⊢⋆ᵗ_ Θ : Kind -> Set where
    Ø   : Θ ⊢⋆ᵗ ⋆
    _◁_ : ∀ {σ τ} -> Θ ⊢ᵗ σ -> Θ ⊢⋆ᵗ τ -> Θ ⊢⋆ᵗ σ ⇒ᵏ τ

mutual
  ren∙ᵗ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢∙ᵗ σ -> Ξ ⊢∙ᵗ σ
  ren∙ᵗ ι (Var v) = Var (renᵛ ι v)
  ren∙ᵗ ι (Fix β) = Fix (renᵗ (keep ι) β)

  renᵗ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢ᵗ σ -> Ξ ⊢ᵗ σ
  renᵗ ι (Lam β)    = Lam (renᵗ (keep ι) β)
  renᵗ ι (App h αs) = App (ren∙ᵗ ι h) (ren⋆ᵗ ι αs)
  renᵗ ι (α ⇒ β)    = renᵗ ι α ⇒ renᵗ ι β
  renᵗ ι (π σ α)    = π σ (renᵗ (keep ι) α)

  ren⋆ᵗ : ∀ {Θ Ξ σ} -> Θ ⊆ Ξ -> Θ ⊢⋆ᵗ σ -> Ξ ⊢⋆ᵗ σ
  ren⋆ᵗ ι  Ø       = Ø
  ren⋆ᵗ ι (α ◁ αs) = renᵗ ι α ◁ ren⋆ᵗ ι αs

shiftᵗ : ∀ {Θ σ τ} -> Θ ⊢ᵗ σ -> Θ ▻ᵏ τ ⊢ᵗ σ
shiftᵗ = renᵗ top

open module TypeCon Θ = Context (Type Θ)

shiftᶜ : ∀ {Θ σ} -> Con Θ -> Con (Θ ▻ᵏ σ)
shiftᶜ = mapᶜ shiftᵗ

module _ where
  infixl 9 _[_]∙ᵗ

  open Environment record
    { renᶠ   = ren∙ᵗ
    ; freshᶠ = Var vz
    }

  mutual
    sub∙̇ᵗ : ∀ {Ξ Θ σ} -> Ξ ⊢ᵉ Θ -> Θ ⊢∙ᵗ σ -> Ξ ⊢∙ᵗ σ
    sub∙̇ᵗ ρ (Var v) = lookupᵉ v ρ
    sub∙̇ᵗ ρ (Fix β) = Fix (suḃᵗ (keepᵉ ρ) β)

    suḃᵗ : ∀ {Ξ Θ σ} -> Ξ ⊢ᵉ Θ -> Θ ⊢ᵗ σ -> Ξ ⊢ᵗ σ
    suḃᵗ ρ (Lam β)    = Lam (suḃᵗ (keepᵉ ρ) β)
    suḃᵗ ρ (App h αs) = App (sub∙̇ᵗ ρ h) (sub⋆̇ᵗ ρ αs)
    suḃᵗ ρ (α ⇒ β)    = suḃᵗ ρ α ⇒ suḃᵗ ρ β
    suḃᵗ ρ (π σ α)    = π σ (suḃᵗ (keepᵉ ρ) α)

    sub⋆̇ᵗ : ∀ {Ξ Θ σ} -> Ξ ⊢ᵉ Θ -> Θ ⊢⋆ᵗ σ -> Ξ ⊢⋆ᵗ σ
    sub⋆̇ᵗ ρ  Ø       = Ø
    sub⋆̇ᵗ ρ (α ◁ αs) = suḃᵗ ρ α ◁ sub⋆̇ᵗ ρ αs

  -- Substitute a head for a variable.
  _[_]∙ᵗ : ∀ {Θ σ τ} -> Θ ▻ᵏ σ ⊢ᵗ τ -> Θ ⊢∙ᵗ σ -> Θ ⊢ᵗ τ
  β [ α ]∙ᵗ = suḃᵗ (topᵉ α) β

mutual
  postulate
    -- Substitute a term for a variable. Entirely standard hereditary substitution stuff.
    _[_]ᵗ : ∀ {Θ σ τ} -> Θ ▻ᵏ σ ⊢ᵗ τ -> Θ ⊢ᵗ σ -> Θ ⊢ᵗ τ

  -- Computing type function (always a type lambda) application.
  _·ᵗ_ : ∀ {Θ σ τ} -> Θ ⊢ᵗ σ ⇒ᵏ τ -> Θ ⊢ᵗ σ -> Θ ⊢ᵗ τ
  Lam β ·ᵗ α = β [ α ]ᵗ

  -- Computing application of a type to a spine.
  App⋆ : ∀ {Θ σ} -> Θ ⊢ᵗ σ -> Θ ⊢⋆ᵗ σ -> Θ ⊢ᵗ ⋆
  App⋆ β  Ø       = β
  App⋆ β (α ◁ αs) = App⋆ (β ·ᵗ α) αs

data _⊢_ {Θ} Γ : Type Θ -> Set where
  var  : ∀ {α}   -> α ∈ Γ -> Γ ⊢ α
  Λ_   : ∀ {σ α} -> shiftᶜ Γ ⊢ α -> Γ ⊢ π σ α
  _[_] : ∀ {σ β} -> Γ ⊢ π σ β -> (α : Θ ⊢ᵗ σ) -> Γ ⊢ β [ α ]ᵗ
  ƛ_   : ∀ {α β} -> Γ ▻ α ⊢ β -> Γ ⊢ α ⇒ β
  _·_  : ∀ {α β} -> Γ ⊢ α ⇒ β -> Γ ⊢ α -> Γ ⊢ β
  wrap   : ∀ {σ ω} {αs : Θ ⊢⋆ᵗ σ} -> Γ ⊢ App⋆ (ω [ Fix ω ]∙ᵗ) αs -> Γ ⊢ App (Fix ω) αs
  unwrap : ∀ {σ ω} {αs : Θ ⊢⋆ᵗ σ} -> Γ ⊢ App (Fix ω) αs -> Γ ⊢ App⋆ (ω [ Fix ω ]∙ᵗ) αs