DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add some additional 'equivalence' definitions to Equivalence

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-18 21:46:42 -08:00
parent 6384f7006e
commit 8c9f39ac35
1 changed files with 15 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Equivalence.agda
View File

@ -4,8 +4,18 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Relation.Binary.Definitions open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where module _ {a} (A : Set a) (_≈_ : A → A → Set a) where
field IsReflexive : Set a
≈-refl : {a : A} → a ≈ a IsReflexive = ∀ {a : A} → a ≈ a
≈-sym : {a b : A} → a ≈ b → b ≈ a
≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c 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