Define syntax and equivalence.

1 files changed, 309 insertions, 0 deletions

diff --git a/src/CBPV/Term.agda b/src/CBPV/Term.agda
new file mode 100644
index 0000000..ec05de4
--- /dev/null
+++ b/src/CBPV/Term.agda
@@ -0,0 +1,309 @@
+{-# 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 ∘′ ∈-++⁺ˡ))
+      })