From bea2f2293dcce6e9f5cde48195755b04b4589df4 Mon Sep 17 00:00:00 2001 From: James McKinna Date: Mon, 6 May 2024 11:41:51 +0100 Subject: [PATCH] refactored to lift out `isEquivalence` --- .../Relation/Binary/Setoid/Equality.agda | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/Function/Relation/Binary/Setoid/Equality.agda b/src/Function/Relation/Binary/Setoid/Equality.agda index 2631d83da9..9d0e9823da 100644 --- a/src/Function/Relation/Binary/Setoid/Equality.agda +++ b/src/Function/Relation/Binary/Setoid/Equality.agda @@ -15,6 +15,8 @@ module Function.Relation.Binary.Setoid.Equality {a₁ a₂ b₁ b₂ : Level} open import Function.Bundles using (Func; _⟨$⟩_) open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive) +open import Relation.Binary.Structures + using (IsEquivalence) private module To = Setoid To @@ -33,17 +35,16 @@ sym = λ f≈g → To.sym f≈g trans : Transitive _≈_ trans = λ f≈g g≈h → To.trans f≈g g≈h -setoid : Setoid _ _ -setoid = record - { Carrier = Func From To - ; _≈_ = _≈_ - ; isEquivalence = record -- need to η-expand else Agda gets confused - { refl = λ {f} → refl {f} - ; sym = λ {f} {g} → sym {f} {g} - ; trans = λ {f} {g} {h} → trans {f} {g} {h} - } +isEquivalence : IsEquivalence _≈_ +isEquivalence = record -- need to η-expand else Agda gets confused + { refl = λ {f} → refl {f} + ; sym = λ {f} {g} → sym {f} {g} + ; trans = λ {f} {g} {h} → trans {f} {g} {h} } +setoid : Setoid _ _ +setoid = record { isEquivalence = isEquivalence } + -- most of the time, this infix version is nicer to use infixr 9 _⇨_ _⇨_ : Setoid _ _