WIP: concrete families

1 files changed, 0 insertions, 309 deletions

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