From 8c9f39ac354c67e3b33cd274432903a0131b9558 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 18 Feb 2024 21:46:42 -0800 Subject: [PATCH] Add some additional 'equivalence' definitions to Equivalence Signed-off-by: Danila Fedorin --- Equivalence.agda | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/Equivalence.agda b/Equivalence.agda index a17a438..c72631e 100644 --- a/Equivalence.agda +++ b/Equivalence.agda @@ -4,8 +4,18 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym) -record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where - field - ≈-refl : {a : A} → a ≈ a - ≈-sym : {a b : A} → a ≈ b → b ≈ a - ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c +module _ {a} (A : Set a) (_≈_ : A → A → Set a) where + IsReflexive : Set a + IsReflexive = ∀ {a : A} → a ≈ a + + IsSymmetric : Set a + IsSymmetric = ∀ {a b : A} → a ≈ b → b ≈ a + + IsTransitive : Set a + IsTransitive = ∀ {a b c : A} → a ≈ b → b ≈ c → a ≈ c + + record IsEquivalence : Set a where + field + ≈-refl : IsReflexive + ≈-sym : IsSymmetric + ≈-trans : IsTransitive