From bf5fedb51726f62aa8f46505ebee87912ef10ce3 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 28 Dec 2023 12:41:57 +0000
Subject: Define syntax and equivalence.

---
 src/CBPV/Equality.agda | 174 +++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 174 insertions(+)
 create mode 100644 src/CBPV/Equality.agda

(limited to 'src/CBPV/Equality.agda')

diff --git a/src/CBPV/Equality.agda b/src/CBPV/Equality.agda
new file mode 100644
index 0000000..f6f58c8
--- /dev/null
+++ b/src/CBPV/Equality.agda
@@ -0,0 +1,174 @@
+{-# 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) []
-- 
cgit v1.2.3