From e98be8390fccbbb2c0aeb2ab50f8e8696bc11847 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Wed, 13 Jul 2022 17:13:54 +0100 Subject: Prove alpha equivalence is an equivalence. --- src/Data/Type/Properties.agda | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'src') diff --git a/src/Data/Type/Properties.agda b/src/Data/Type/Properties.agda index 16f6d8e..0ef018f 100644 --- a/src/Data/Type/Properties.agda +++ b/src/Data/Type/Properties.agda @@ -27,6 +27,7 @@ open import Relation.Binary hiding (_⇔_) import Relation.Binary.Construct.On as On using (wellFounded) open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; _≗_; sym; cong; cong₂; module ≡-Reasoning) +import Relation.Binary.Reasoning.Setoid as Reasoning open import Relation.Nullary using (Dec; Reflects; ¬_; _because_; yes; no) open import Relation.Nullary.Negation using (¬?; decidable-stable) @@ -262,3 +263,18 @@ free-≈ (all {α} {A} {β} {B} A≈B) = begin all (λ δ∉∀α∙A δ∉∀γ∙C → ≈-trans (A≈B δ∉∀α∙A (P.subst (_ ∉_) (free-≈ (all A≈B)) δ∉∀α∙A)) (B≈C (P.subst (_ ∉_) (sym (free-≈ (all B≈C))) δ∉∀γ∙C) δ∉∀γ∙C)) + +≈-isEquivalence : IsEquivalence _≈_ +≈-isEquivalence = record + { refl = ≈-refl + ; sym = ≈-sym + ; trans = ≈-trans + } + +open IsEquivalence ≈-isEquivalence public + using () renaming (reflexive to ≈-reflexive) + +≈-setoid : Setoid _ _ +≈-setoid = record { isEquivalence = ≈-isEquivalence } + +module ≈-Reasoning = Reasoning ≈-setoid -- cgit v1.2.3