From bf5fedb51726f62aa8f46505ebee87912ef10ce3 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Thu, 28 Dec 2023 12:41:57 +0000 Subject: Define syntax and equivalence. --- src/CBPV/Term.agda | 309 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 309 insertions(+) create mode 100644 src/CBPV/Term.agda (limited to 'src/CBPV/Term.agda') 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 ∘′ ∈-++⁺ˡ)) + }) -- cgit v1.2.3