open import Graded.Modality
module Graded.Context.Properties.Equivalence
{a} {M : Set a} (𝕄 : Modality M) where
open import Graded.Context 𝕄
open import Tools.Function
open import Tools.Nat
open import Tools.PropositionalEquality
import Tools.Reasoning.Equivalence
open import Tools.Relation
open Modality 𝕄
private
variable
n : Nat
γ δ η : Conₘ n
≈ᶜ-refl : γ ≈ᶜ γ
≈ᶜ-refl {γ = ε} = ε
≈ᶜ-refl {γ = γ ∙ p} = ≈ᶜ-refl ∙ refl
≈ᶜ-trans : γ ≈ᶜ δ → δ ≈ᶜ η → γ ≈ᶜ η
≈ᶜ-trans {γ = ε} {δ = ε} {η = ε} _ _ = ε
≈ᶜ-trans {γ = _ ∙ _} {δ = _ ∙ _} {η = _ ∙ _} (γ≈δ ∙ p≡q) (δ≈η ∙ q≡r) =
≈ᶜ-trans γ≈δ δ≈η ∙ trans p≡q q≡r
≈ᶜ-sym : γ ≈ᶜ δ → δ ≈ᶜ γ
≈ᶜ-sym {γ = ε} {δ = ε} _ = ε
≈ᶜ-sym {γ = _ ∙ _} {δ = _ ∙ _} (γ≈δ ∙ p≡q) = ≈ᶜ-sym γ≈δ ∙ sym p≡q
≈ᶜ-equivalence : {n : Nat} → IsEquivalence (_≈ᶜ_ {n = n})
≈ᶜ-equivalence = record
{ refl = ≈ᶜ-refl
; sym = ≈ᶜ-sym
; trans = ≈ᶜ-trans
}
Conₘ-setoid : {n : Nat} → Setoid a a
Conₘ-setoid {n} = record
{ Carrier = Conₘ n ; _≈_ = _≈ᶜ_ ; isEquivalence = ≈ᶜ-equivalence }
module ≈ᶜ-reasoning {n : Nat} =
Tools.Reasoning.Equivalence (Conₘ-setoid {n = n})
≈ᶜ→≡ : γ ≈ᶜ δ → γ ≡ δ
≈ᶜ→≡ ε = refl
≈ᶜ→≡ (ps ∙ refl) = cong (_∙ _) (≈ᶜ→≡ ps)
≈ᶜ-decidable : Decidable (_≡_ {A = M}) → Decidable (_≈ᶜ_ {n = n})
≈ᶜ-decidable _≡?_ = λ where
ε ε → yes ε
(γ ∙ p) (δ ∙ q) → case p ≡? q of λ where
(no p≢q) → no λ where
(_ ∙ p≡q) → p≢q p≡q
(yes p≡q) → case ≈ᶜ-decidable _≡?_ γ δ of λ where
(no γ≉ᶜδ) → no λ where
(γ≈ᶜδ ∙ _) → γ≉ᶜδ γ≈ᶜδ
(yes γ≈ᶜδ) → yes (γ≈ᶜδ ∙ p≡q)