Prove alpha equivalence is an equivalence.

1 files changed, 16 insertions, 0 deletions

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