WIP: concrete families

1 files changed, 0 insertions, 174 deletions

diff --git a/src/CBPV/Equality.agda b/src/CBPV/Equality.agda
deleted file mode 100644
index f6f58c8..0000000
--- a/src/CBPV/Equality.agda
+++ /dev/null
@@ -1,174 +0,0 @@
-{-# OPTIONS --safe #-}
-
-module CBPV.Equality where
-
-open import Data.List using (List; []; _∷_; _++_)
-open import Data.List.Membership.Propositional using (_∈_)
-open import Data.List.Relation.Unary.All using (All; _∷_; []; lookup)
-open import Data.List.Relation.Unary.Any using (here; there)
-open import Data.Product using () renaming (_×_ to _×′_; _,_ to _,′_)
-open import Level using (0ℓ)
-open import Relation.Binary using (Rel; _⇒_; _=[_]⇒_; Reflexive; Symmetric; Transitive; Setoid)
-open import Relation.Binary.PropositionalEquality using (refl)
-import Relation.Binary.Reasoning.Setoid as SetoidReasoning
-
-open import CBPV.Axiom
-open import CBPV.Family
-open import CBPV.Term
-open import CBPV.Type
-
-private
-  variable
-    Vs Vs′ : List (Context ×′ ValType)
-    Cs Cs′ : List (Context ×′ CompType)
-    Γ Δ : Context
-    A A′ : ValType
-    B B′ : CompType
-
-infix 0 _⨾_▹_⊢ᵛ_≈_ _⨾_▹_⊢ᶜ_≈_
-
-data _⨾_▹_⊢ᵛ_≈_ : ∀ Vs Cs Γ {A} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A) 0ℓ
-data _⨾_▹_⊢ᶜ_≈_ : ∀ Vs Cs Γ {B} → Rel (⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B) 0ℓ
-
-data _⨾_▹_⊢ᵛ_≈_ where
-  refl  : Reflexive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
-  sym   : Symmetric {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
-  trans : Transitive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_)
-  axiom : (_⨾_▹⊢ᵛ_≋_ Vs Cs {A}) ⇒ (Vs ⨾ Cs ▹ [] ⊢ᵛ_≈_)
-  ren   : (ρ : Γ ~[ I ]↝ᵛ Δ) → (Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_) =[ renᵛ {A = A} ρ ]⇒ (Vs ⨾ Cs ▹ Δ ⊢ᵛ_≈_)
-  msub  :
-    {val₁ val₂ : ⌞ Vs ⌟ᵛ ⇒ᵛ δᵛ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᵛ_)}
-    {comp₁ comp₂ : ⌞ Cs ⌟ᶜ ⇒ᶜ δᶜ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᶜ_)}
-    {t u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A} →
-    (∀ {A Δ} → (m : (Δ ,′ A) ∈ Vs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᵛ val₁ m ≈ val₂ m) →
-    (∀ {B Δ} → (m : (Δ ,′ B) ∈ Cs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᶜ comp₁ m ≈ comp₂ m) →
-    Vs ⨾ Cs ▹ Γ ⊢ᵛ t ≈ u →
-    Vs′ ⨾ Cs′ ▹ Γ ⊢ᵛ msubᵛ val₁ comp₁ t ≈ msubᵛ val₂ comp₂ u
-
-data _⨾_▹_⊢ᶜ_≈_ where
-  refl  : Reflexive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
-  sym   : Symmetric {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
-  trans : Transitive {A = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_)
-  axiom : (_⨾_▹⊢ᶜ_≋_ Vs Cs {B}) ⇒ (Vs ⨾ Cs ▹ [] ⊢ᶜ_≈_)
-  ren   : (ρ : Γ ~[ I ]↝ᵛ Δ) → (Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_) =[ renᶜ {B = B} ρ ]⇒ (Vs ⨾ Cs ▹ Δ ⊢ᶜ_≈_)
-  msub  :
-    {val₁ val₂ : ⌞ Vs ⌟ᵛ ⇒ᵛ δᵛ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᵛ_)}
-    {comp₁ comp₂ : ⌞ Cs ⌟ᶜ ⇒ᶜ δᶜ Γ (⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹_⊢ᶜ_)}
-    {t u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B} →
-    (∀ {A Δ} → (m : (Δ ,′ A) ∈ Vs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᵛ val₁ m ≈ val₂ m) →
-    (∀ {B Δ} → (m : (Δ ,′ B) ∈ Cs) → Vs′ ⨾ Cs′ ▹ Δ ++ Γ ⊢ᶜ comp₁ m ≈ comp₂ m) →
-    Vs ⨾ Cs ▹ Γ ⊢ᶜ t ≈ u →
-    Vs′ ⨾ Cs′ ▹ Γ ⊢ᶜ msubᶜ val₁ comp₁ t ≈ msubᶜ val₂ comp₂ u
-
-≈ᵛ-setoid :
-  (Vs : List (Context ×′ ValType)) (Cs : List (Context ×′ CompType)) (Γ : Context) (A : ValType) →
-  Setoid 0ℓ 0ℓ
-≈ᵛ-setoid Vs Cs Γ A = record
-  { Carrier = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A
-  ; _≈_ = Vs ⨾ Cs ▹ Γ ⊢ᵛ_≈_
-  ; isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
-  }
-
-≈ᶜ-setoid :
-  (Vs : List (Context ×′ ValType)) (Cs : List (Context ×′ CompType)) (Γ : Context) (B : CompType) →
-  Setoid 0ℓ 0ℓ
-≈ᶜ-setoid Vs Cs Γ B = record
-  { Carrier = ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B
-  ; _≈_ = Vs ⨾ Cs ▹ Γ ⊢ᶜ_≈_
-  ; isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
-  }
-
-module ValReasoning {Vs} {Cs} {Γ} {A} = SetoidReasoning (≈ᵛ-setoid Vs Cs Γ A)
-module CompReasoning {Vs} {Cs} {Γ} {B} = SetoidReasoning (≈ᶜ-setoid Vs Cs Γ B)
-
--- Congruence
-
-val-congᵛ :
-  (t : ⌞ (Δ ,′ A′) ∷ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A)
-  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A′} →
-  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᵛ s ≈ u →
-  Vs ⨾ Cs ▹ Γ ⊢ᵛ val-instᵛ s t ≈ val-instᵛ u t
-val-congᵛ t s≈u =
-  msub {t = t}
-    (λ
-      { (here refl) → s≈u
-      ; (there m)   → refl
-      })
-    (λ m → refl)
-    refl
-
-val-congᶜ :
-  (t : ⌞ (Δ ,′ A) ∷ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B)
-  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A} →
-  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᵛ s ≈ u →
-  Vs ⨾ Cs ▹ Γ ⊢ᶜ val-instᶜ s t ≈ val-instᶜ u t
-val-congᶜ t s≈u =
-  msub {t = t}
-    (λ
-      { (here refl) → s≈u
-      ; (there m)   → refl
-      })
-    (λ m → refl)
-    refl
-
-comp-congᵛ :
-  (t : ⌞ Vs ⌟ᵛ ⨾ ⌞ (Δ ,′ B) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A)
-  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B} →
-  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᶜ s ≈ u →
-  Vs ⨾ Cs ▹ Γ ⊢ᵛ comp-instᵛ s t ≈ comp-instᵛ u t
-comp-congᵛ t s≈u =
-  msub {t = t}
-    (λ m → refl)
-    (λ
-      { (here refl) → s≈u
-      ; (there m)   → refl
-      })
-    refl
-
-comp-congᶜ :
-  (t : ⌞ Vs ⌟ᵛ ⨾ ⌞ (Δ ,′ B′) ∷ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B)
-  {s u : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B′} →
-  Vs ⨾ Cs ▹ Δ ++ Γ ⊢ᶜ s ≈ u →
-  Vs ⨾ Cs ▹ Γ ⊢ᶜ comp-instᶜ s t ≈ comp-instᶜ u t
-comp-congᶜ t s≈u =
-  msub {t = t}
-    (λ m → refl)
-    (λ
-      { (here refl) → s≈u
-      ; (there m)   → refl
-      })
-    refl
-
-thmᵛ≈ :
-  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᵛ A}
-  (thm : Vs ⨾ Cs ▹ Γ ⊢ᵛ t ≈ s)
-  (ρ : All (I Δ) Γ)
-  (ζ : All (λ (Θ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᵛ A) Vs)
-  (ξ : All (λ (Θ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᶜ B) Cs) →
-  Vs′ ⨾ Cs′ ▹ Δ ⊢ᵛ msub′ᵛ ζ ξ (ren′ᵛ ρ t) ≈ msub′ᵛ ζ ξ (ren′ᵛ ρ s)
-thmᵛ≈ thm ρ ζ ξ = msub (λ _ → refl) (λ _ → refl) (ren (lookup ρ) thm)
-
-thmᶜ≈ :
-  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ Γ ⊢ᶜ B}
-  (thm : Vs ⨾ Cs ▹ Γ ⊢ᶜ t ≈ s)
-  (ρ : All (I Δ) Γ)
-  (ζ : All (λ (Θ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᵛ A) Vs)
-  (ξ : All (λ (Θ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Θ ++ Δ ⊢ᶜ B) Cs) →
-  Vs′ ⨾ Cs′ ▹ Δ ⊢ᶜ msub′ᶜ ζ ξ (ren′ᶜ ρ t) ≈ msub′ᶜ ζ ξ (ren′ᶜ ρ s)
-thmᶜ≈ thm ρ ζ ξ = msub (λ _ → refl) (λ _ → refl) (ren (lookup ρ) thm)
-
-axᵛ≈ :
-  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᵛ A}
-  (ax : Vs ⨾ Cs ▹⊢ᵛ t ≋ s)
-  (ζ : All (λ (Δ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A) Vs)
-  (ξ : All (λ (Δ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B) Cs) →
-  Vs′ ⨾ Cs′ ▹ Γ ⊢ᵛ msub′ᵛ ζ ξ (ren′ᵛ [] t) ≈ msub′ᵛ ζ ξ (ren′ᵛ [] s)
-axᵛ≈ ax = thmᵛ≈ (axiom ax) []
-
-axᶜ≈ :
-  {t s : ⌞ Vs ⌟ᵛ ⨾ ⌞ Cs ⌟ᶜ ▹ [] ⊢ᶜ B}
-  (ax : Vs ⨾ Cs ▹⊢ᶜ t ≋ s)
-  (ζ : All (λ (Δ ,′ A) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᵛ A) Vs)
-  (ξ : All (λ (Δ ,′ B) → ⌞ Vs′ ⌟ᵛ ⨾ ⌞ Cs′ ⌟ᶜ ▹ Δ ++ Γ ⊢ᶜ B) Cs) →
-  Vs′ ⨾ Cs′ ▹ Γ ⊢ᶜ msub′ᶜ ζ ξ (ren′ᶜ [] t) ≈ msub′ᶜ ζ ξ (ren′ᶜ [] s)
-axᶜ≈ ax = thmᶜ≈ (axiom ax) []