agda-spa/Equivalence.agda
Danila Fedorin 8c9f39ac35 Add some additional 'equivalence' definitions to Equivalence
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-18 21:46:42 -08:00

22 lines
670 B
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Equivalence where
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
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