{-# OPTIONS --safe #-}

module CBPV.Term where

open import Data.List using (List; []; _∷_; [_]; _++_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties using (∈-++⁻; ∈-++⁺ˡ; ∈-++⁺ʳ)
open import Data.List.Relation.Unary.All using (All; []; _∷_; lookup; tabulate)
open import Data.List.Relation.Unary.All.Properties using () renaming (++⁺ to _++⁺_)
open import Data.List.Relation.Unary.Any using (here; there)
open import Data.Product using () renaming (_×_ to _×′_; _,_ to _,′_)
open import Data.Sum using ([_,_]′)
open import Function.Base using (id; _∘_; _∘′_)
open import Level using (Level; _⊔_)
open import Relation.Binary.PropositionalEquality using (refl)

open import CBPV.Family
open import CBPV.Type

private
  variable
    Γ Δ : Context
    A A′ A′′ : ValType
    B B′ : CompType
    As : List ValType

infix 0 _⨾_▹_⊢ᵛ_ _⨾_▹_⊢ᶜ_
infix 9 ƛ_
infixr 8 _‵_
infixr 2 _,_
infixr 1 have_be_ _to_

data _⨾_▹_⊢ᵛ_ {v c} (V : ValFamily v) (C : CompFamily c) (Γ : Context) : ValType → Set (v ⊔ c)
data _⨾_▹_⊢ᶜ_ {v c} (V : ValFamily v) (C : CompFamily c) (Γ : Context) : CompType → Set (v ⊔ c)

data _⨾_▹_⊢ᵛ_ V C Γ where
  -- Initiality
  mvar : V Δ A → All (V ⨾ C ▹ Γ ⊢ᵛ_) Δ → V ⨾ C ▹ Γ ⊢ᵛ A
  var  : A ∈ Γ → V ⨾ C ▹ Γ ⊢ᵛ A
  -- Structural
  have_be_ : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ A ∷ Γ ⊢ᵛ A′ → V ⨾ C ▹ Γ ⊢ᵛ A′
  -- Introductors
  thunk : V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᵛ U B
  tt    : V ⨾ C ▹ Γ ⊢ᵛ 𝟙
  inl   : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A + A′
  inr   : V ⨾ C ▹ Γ ⊢ᵛ A′ → V ⨾ C ▹ Γ ⊢ᵛ A + A′
  _,_   : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A′ → V ⨾ C ▹ Γ ⊢ᵛ A × A′
  ƛ_    : V ⨾ C ▹ A ∷ Γ ⊢ᵛ A′ → V ⨾ C ▹ Γ ⊢ᵛ A ⟶ A′
  -- Eliminators
  absurd  : V ⨾ C ▹ Γ ⊢ᵛ 𝟘 → V ⨾ C ▹ Γ ⊢ᵛ A
  unpoint : V ⨾ C ▹ Γ ⊢ᵛ 𝟙 → V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A
  untag   : V ⨾ C ▹ Γ ⊢ᵛ A + A′ → V ⨾ C ▹ A ∷ Γ ⊢ᵛ A′′ → V ⨾ C ▹ A′ ∷ Γ ⊢ᵛ A′′ → V ⨾ C ▹ Γ ⊢ᵛ A′′
  unpair  : V ⨾ C ▹ Γ ⊢ᵛ A × A′ → V ⨾ C ▹ A ∷ A′ ∷ Γ ⊢ᵛ A′′ → V ⨾ C ▹ Γ ⊢ᵛ A′′
  _‵_     : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A ⟶ A′ → V ⨾ C ▹ Γ ⊢ᵛ A′

data _⨾_▹_⊢ᶜ_ V C Γ where
  -- Initiality
  mvar : C Δ B → All (V ⨾ C ▹ Γ ⊢ᵛ_) Δ → V ⨾ C ▹ Γ ⊢ᶜ B
  -- Structural
  have_be_ : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ A ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
  -- Introductors
  return : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᶜ F A
  tt     : V ⨾ C ▹ Γ ⊢ᶜ 𝟙
  _,_    : V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B′ → V ⨾ C ▹ Γ ⊢ᶜ B × B′
  ƛ_     : V ⨾ C ▹ A ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ A ⟶ B
  -- Eliminators
  force   : V ⨾ C ▹ Γ ⊢ᵛ U B → V ⨾ C ▹ Γ ⊢ᶜ B
  absurd  : V ⨾ C ▹ Γ ⊢ᵛ 𝟘 → V ⨾ C ▹ Γ ⊢ᶜ B
  unpoint : V ⨾ C ▹ Γ ⊢ᵛ 𝟙 → V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
  untag   : V ⨾ C ▹ Γ ⊢ᵛ A + A′ → V ⨾ C ▹ A ∷ Γ ⊢ᶜ B → V ⨾ C ▹ A′ ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
  unpair  : V ⨾ C ▹ Γ ⊢ᵛ A × A′ → V ⨾ C ▹ A ∷ A′ ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
  _to_    : V ⨾ C ▹ Γ ⊢ᶜ F A → V ⨾ C ▹ A ∷ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
  π₁      : V ⨾ C ▹ Γ ⊢ᶜ B × B′ → V ⨾ C ▹ Γ ⊢ᶜ B
  π₂      : V ⨾ C ▹ Γ ⊢ᶜ B × B′ → V ⨾ C ▹ Γ ⊢ᶜ B′
  _‵_     : V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᶜ A ⟶ B → V ⨾ C ▹ Γ ⊢ᶜ B

private
  variable
    ℓ : Level
    V V′ : ValFamily ℓ
    C C′ : CompFamily ℓ
    Vs : List (Context ×′ ValType)
    Cs : List (Context ×′ CompType)

lift :
  (V : ValFamily ℓ) →
  (∀ {A Γ Δ} → Γ ~[ I ]↝ᵛ Δ → V Γ A → V Δ A) →
  I ⇒ᵛ V →
  (Θ : Context) →
  Γ ~[ V ]↝ᵛ Δ →
  Θ ++ Γ ~[ V ]↝ᵛ Θ ++ Δ
lift V ren new Θ σ = [ new ∘′ ∈-++⁺ˡ , ren (∈-++⁺ʳ Θ) ∘′ σ ]′ ∘′ ∈-++⁻ Θ

liftI : (Θ : Context) → Γ ~[ I ]↝ᵛ Δ → Θ ++ Γ ~[ I ]↝ᵛ Θ ++ Δ
liftI = lift I (λ f → f) id

-- Renaming --------------------------------------------------------------------

renᵛ : Δ ~[ I ]↝ᵛ Γ → V ⨾ C ▹ Δ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A
renᶜ : Δ ~[ I ]↝ᵛ Γ → V ⨾ C ▹ Δ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
renᵛ⋆ : Δ ~[ I ]↝ᵛ Γ → All (V ⨾ C ▹ Δ ⊢ᵛ_) As → All (V ⨾ C ▹ Γ ⊢ᵛ_) As

renᵛ ρ (mvar m ts)  = mvar m (renᵛ⋆ ρ ts)
renᵛ ρ (var i)      = var (ρ i)

renᵛ ρ (have t be s) = have renᵛ ρ t be renᵛ (liftI [ _ ] ρ) s

renᵛ ρ (thunk t) = thunk (renᶜ ρ t)
renᵛ ρ tt        = tt
renᵛ ρ (inl t)   = inl (renᵛ ρ t)
renᵛ ρ (inr t)   = inr (renᵛ ρ t)
renᵛ ρ (t , s)   = renᵛ ρ t , renᵛ ρ s
renᵛ ρ (ƛ t)     = ƛ renᵛ (liftI [ _ ] ρ) t

renᵛ ρ (absurd t)    = absurd (renᵛ ρ t)
renᵛ ρ (unpoint t s) = unpoint (renᵛ ρ t) (renᵛ ρ s)
renᵛ ρ (untag t s u) = untag (renᵛ ρ t) (renᵛ (liftI [ _ ] ρ) s) (renᵛ (liftI [ _ ] ρ) u)
renᵛ ρ (unpair t s)  = unpair (renᵛ ρ t) (renᵛ (liftI (_ ∷ _ ∷ []) ρ) s)
renᵛ ρ (t ‵ s)       = renᵛ ρ t ‵ renᵛ ρ s

renᶜ ρ (mvar m ts) = mvar m (renᵛ⋆ ρ ts)

renᶜ ρ (have t be s) = have renᵛ ρ t be renᶜ (liftI [ _ ] ρ) s

renᶜ ρ (return t) = return (renᵛ ρ t)
renᶜ ρ tt         = tt
renᶜ ρ (t , s)    = renᶜ ρ t , renᶜ ρ s
renᶜ ρ (ƛ t)      = ƛ renᶜ (liftI [ _ ] ρ) t

renᶜ ρ (force t)     = force (renᵛ ρ t)
renᶜ ρ (absurd t)    = absurd (renᵛ ρ t)
renᶜ ρ (unpoint t s) = unpoint (renᵛ ρ t) (renᶜ ρ s)
renᶜ ρ (untag t s u) = untag (renᵛ ρ t) (renᶜ (liftI [ _ ] ρ) s) (renᶜ (liftI [ _ ] ρ) u)
renᶜ ρ (unpair t s)  = unpair (renᵛ ρ t) (renᶜ (liftI (_ ∷ _ ∷ []) ρ) s)
renᶜ ρ (t to s)      = renᶜ ρ t to renᶜ (liftI [ _ ] ρ) s
renᶜ ρ (π₁ t)        = π₁ (renᶜ ρ t)
renᶜ ρ (π₂ t)        = π₂ (renᶜ ρ t)
renᶜ ρ (t ‵ s)       = renᵛ ρ t ‵ renᶜ ρ s

renᵛ⋆ ρ []       = []
renᵛ⋆ ρ (t ∷ ts) = renᵛ ρ t ∷ renᵛ⋆ ρ ts

-- Shorthand

ren′ᵛ : All (I Δ) Γ → V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Δ ⊢ᵛ A
ren′ᵛ ρ = renᵛ (lookup ρ)

ren′ᶜ : All (I Δ) Γ → V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Δ ⊢ᶜ B
ren′ᶜ ρ = renᶜ (lookup ρ)

liftV : (Θ : Context) → Γ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Δ → Θ ++ Γ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Θ ++ Δ
liftV = lift (_ ⨾ _ ▹_⊢ᵛ_) renᵛ var

-- Substitution ----------------------------------------------------------------

subᵛ : Δ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Γ → V ⨾ C ▹ Δ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A
subᶜ : Δ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Γ → V ⨾ C ▹ Δ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
subᵛ⋆ : Δ ~[ V ⨾ C ▹_⊢ᵛ_ ]↝ᵛ Γ → All (V ⨾ C ▹ Δ ⊢ᵛ_) As → All (V ⨾ C ▹ Γ ⊢ᵛ_) As

subᵛ σ (mvar m ts)  = mvar m (subᵛ⋆ σ ts)
subᵛ σ (var i)      = σ i

subᵛ σ (have t be s) = have subᵛ σ t be subᵛ (liftV [ _ ] σ) s

subᵛ σ (thunk t) = thunk (subᶜ σ t)
subᵛ σ tt        = tt
subᵛ σ (inl t)   = inl (subᵛ σ t)
subᵛ σ (inr t)   = inr (subᵛ σ t)
subᵛ σ (t , s)   = subᵛ σ t , subᵛ σ s
subᵛ σ (ƛ t)     = ƛ subᵛ (liftV [ _ ] σ) t

subᵛ σ (absurd t)    = absurd (subᵛ σ t)
subᵛ σ (unpoint t s) = unpoint (subᵛ σ t) (subᵛ σ s)
subᵛ σ (untag t s u) = untag (subᵛ σ t) (subᵛ (liftV [ _ ] σ) s) (subᵛ (liftV [ _ ] σ) u)
subᵛ σ (unpair t s)  = unpair (subᵛ σ t) (subᵛ (liftV (_ ∷ _ ∷ []) σ) s)
subᵛ σ (t ‵ s)       = subᵛ σ t ‵ subᵛ σ s

subᶜ σ (mvar m ts) = mvar m (subᵛ⋆ σ ts)

subᶜ σ (have t be s) = have subᵛ σ t be subᶜ (liftV [ _ ] σ) s

subᶜ σ (return t) = return (subᵛ σ t)
subᶜ σ tt         = tt
subᶜ σ (t , s)    = subᶜ σ t , subᶜ σ s
subᶜ σ (ƛ t)      = ƛ subᶜ (liftV [ _ ] σ) t

subᶜ σ (force t)     = force (subᵛ σ t)
subᶜ σ (absurd t)    = absurd (subᵛ σ t)
subᶜ σ (unpoint t s) = unpoint (subᵛ σ t) (subᶜ σ s)
subᶜ σ (untag t s u) = untag (subᵛ σ t) (subᶜ (liftV [ _ ] σ) s) (subᶜ (liftV [ _ ] σ) u)
subᶜ σ (unpair t s)  = unpair (subᵛ σ t) (subᶜ (liftV (_ ∷ _ ∷ []) σ) s)
subᶜ σ (t to s)      = subᶜ σ t to subᶜ (liftV [ _ ] σ) s
subᶜ σ (π₁ t)        = π₁ (subᶜ σ t)
subᶜ σ (π₂ t)        = π₂ (subᶜ σ t)
subᶜ σ (t ‵ s)       = subᵛ σ t ‵ subᶜ σ s

subᵛ⋆ σ []       = []
subᵛ⋆ σ (t ∷ ts) = subᵛ σ t ∷ subᵛ⋆ σ ts

-- Shorthand

sub′ᵛ : All (V ⨾ C ▹ Δ ⊢ᵛ_) Γ → V ⨾ C ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Δ ⊢ᵛ A
sub′ᵛ ρ = subᵛ (lookup ρ)

sub′ᶜ : All (V ⨾ C ▹ Δ ⊢ᵛ_) Γ → V ⨾ C ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Δ ⊢ᶜ B
sub′ᶜ ρ = subᶜ (lookup ρ)

-- Syntactic Substitution ------------------------------------------------------

wknᵛ : (Θ : Context) → δᵛ Δ (V ⨾ C ▹_⊢ᵛ_) ⇒ᵛ δᵛ (Θ ++ Δ) (V ⨾ C ▹_⊢ᵛ_)
wknᵛ {Δ} Θ {Γ} = renᵛ (liftI Γ (∈-++⁺ʳ Θ))

wknᶜ : (Θ : Context) → δᶜ Δ (V ⨾ C ▹_⊢ᶜ_) ⇒ᶜ δᶜ (Θ ++ Δ) (V ⨾ C ▹_⊢ᶜ_)
wknᶜ {Δ} Θ {Γ} = renᶜ (liftI Γ (∈-++⁺ʳ Θ))

msubᵛ : V ⇒ᵛ δᵛ Γ (V′ ⨾ C′ ▹_⊢ᵛ_) → C ⇒ᶜ δᶜ Γ (V′ ⨾ C′ ▹_⊢ᶜ_) → V ⨾ C ▹ Γ ⊢ᵛ A → V′ ⨾ C′ ▹ Γ ⊢ᵛ A
msubᶜ : V ⇒ᵛ δᵛ Γ (V′ ⨾ C′ ▹_⊢ᵛ_) → C ⇒ᶜ δᶜ Γ (V′ ⨾ C′ ▹_⊢ᶜ_) → V ⨾ C ▹ Γ ⊢ᶜ B → V′ ⨾ C′ ▹ Γ ⊢ᶜ B
msubᵛ⋆ : V ⇒ᵛ δᵛ Γ (V′ ⨾ C′ ▹_⊢ᵛ_) → C ⇒ᶜ δᶜ Γ (V′ ⨾ C′ ▹_⊢ᶜ_) → All (V ⨾ C ▹ Γ ⊢ᵛ_) As → All (V′ ⨾ C′ ▹ Γ ⊢ᵛ_) As

msubᵛ val comp (mvar m ts) = subᵛ (lookup (msubᵛ⋆ val comp ts ++⁺ tabulate var)) (val m)
msubᵛ val comp (var i)     = var i

msubᵛ val comp (have t be s) = have msubᵛ val comp t be msubᵛ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s

msubᵛ val comp (thunk t) = thunk (msubᶜ val comp t)
msubᵛ val comp tt        = tt
msubᵛ val comp (inl t)   = inl (msubᵛ val comp t)
msubᵛ val comp (inr t)   = inr (msubᵛ val comp t)
msubᵛ val comp (t , s)   = msubᵛ val comp t , msubᵛ val comp s
msubᵛ val comp (ƛ t)     = ƛ msubᵛ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) t

msubᵛ val comp (absurd t)    = absurd (msubᵛ val comp t)
msubᵛ val comp (unpoint t s) = unpoint (msubᵛ val comp t) (msubᵛ val comp s)
msubᵛ val comp (untag t s u) = untag (msubᵛ val comp t) (msubᵛ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s) (msubᵛ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) u)
msubᵛ val comp (unpair t s)  = unpair (msubᵛ val comp t) (msubᵛ (wknᵛ (_ ∷ _ ∷ []) ∘′ val) (wknᶜ (_ ∷ _ ∷ []) ∘′ comp) s)
msubᵛ val comp (t ‵ s)       = msubᵛ val comp t ‵ msubᵛ val comp s

msubᶜ val comp (mvar m ts) = subᶜ (lookup (msubᵛ⋆ val comp ts ++⁺ tabulate var)) (comp m)

msubᶜ val comp (have t be s) = have msubᵛ val comp t be msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s

msubᶜ val comp (return t) = return (msubᵛ val comp t)
msubᶜ val comp tt         = tt
msubᶜ val comp (t , s)    = msubᶜ val comp t , msubᶜ val comp s
msubᶜ val comp (ƛ t)      = ƛ msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) t

msubᶜ val comp (force t)     = force (msubᵛ val comp t)
msubᶜ val comp (absurd t)    = absurd (msubᵛ val comp t)
msubᶜ val comp (unpoint t s) = unpoint (msubᵛ val comp t) (msubᶜ val comp s)
msubᶜ val comp (untag t s u) = untag (msubᵛ val comp t) (msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s) (msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) u)
msubᶜ val comp (unpair t s)  = unpair (msubᵛ val comp t) (msubᶜ (wknᵛ (_ ∷ _ ∷ []) ∘′ val) (wknᶜ (_ ∷ _ ∷ []) ∘′ comp) s)
msubᶜ val comp (t to s)      = msubᶜ val comp t to msubᶜ (wknᵛ [ _ ] ∘′ val) (wknᶜ [ _ ] ∘′ comp) s
msubᶜ val comp (π₁ t)        = π₁ (msubᶜ val comp t)
msubᶜ val comp (π₂ t)        = π₂ (msubᶜ val comp t)
msubᶜ val comp (t ‵ s)       = msubᵛ val comp t ‵ msubᶜ val comp s

msubᵛ⋆ val comp []       = []
msubᵛ⋆ val comp (t ∷ ts) = msubᵛ val comp t ∷ msubᵛ⋆ val comp ts

-- Shorthand

msub′ᵛ :
  All (λ (Δ ,′ A) → V ⨾ C ▹ Δ ++ Γ ⊢ᵛ A) Vs →
  All (λ (Δ ,′ B) → V ⨾ C ▹ Δ ++ Γ ⊢ᶜ B) Cs →
  ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A → V ⨾ C ▹ Γ ⊢ᵛ A
msub′ᵛ ζ ξ = msubᵛ (lookup ζ) (lookup ξ)

msub′ᶜ :
  All (λ (Δ ,′ A) → V ⨾ C ▹ Δ ++ Γ ⊢ᵛ A) Vs →
  All (λ (Δ ,′ B) → V ⨾ C ▹ Δ ++ Γ ⊢ᶜ B) Cs →
  ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B → V ⨾ C ▹ Γ ⊢ᶜ B
msub′ᶜ ζ ξ = msubᶜ (lookup ζ) (lookup ξ)

val-instᵛ : ⌞ Vs ⌟ᵛ ⨾ C ▹ Δ ++ Γ ⊢ᵛ A′ → ⌞ (Δ ,′ A′) ∷ Vs ⌟ᵛ ⨾ C ▹ Γ ⊢ᵛ A → ⌞ Vs ⌟ᵛ ⨾ C ▹ Γ ⊢ᵛ A
val-instᵛ t =
  msubᵛ
    (λ
      { (here refl) → t
      ; (there m)   → mvar m (tabulate (var ∘′ ∈-++⁺ˡ))
      })
    (λ m → mvar m (tabulate (var ∘′ ∈-++⁺ˡ)))

val-instᶜ : ⌞ Vs ⌟ᵛ ⨾ C ▹ Δ ++ Γ ⊢ᵛ A → ⌞ (Δ ,′ A) ∷ Vs ⌟ᵛ ⨾ C ▹ Γ ⊢ᶜ B → ⌞ Vs ⌟ᵛ ⨾ C ▹ Γ ⊢ᶜ B
val-instᶜ t =
  msubᶜ
    (λ
      { (here refl) → t
      ; (there m)   → mvar m (tabulate (var ∘′ ∈-++⁺ˡ))
      })
    (λ m → mvar m (tabulate (var ∘′ ∈-++⁺ˡ)))


comp-instᵛ : V ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B → V ⨾ ⌞ (Δ ,′ B) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A → V ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A
comp-instᵛ t =
  msubᵛ
    (λ m → mvar m (tabulate (var ∘′ ∈-++⁺ˡ)))
    (λ
      { (here refl) → t
      ; (there m)   → mvar m (tabulate (var ∘′ ∈-++⁺ˡ))
      })

comp-instᶜ : V ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B′ → V ⨾ ⌞ (Δ ,′ B′) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B → V ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B
comp-instᶜ t =
  msubᶜ
    (λ m → mvar m (tabulate (var ∘′ ∈-++⁺ˡ)))
    (λ
      { (here refl) → t
      ; (there m)   → mvar m (tabulate (var ∘′ ∈-++⁺ˡ))
      })