38 lines
1.5 KiB
Agda
38 lines
1.5 KiB
Agda
|
module Equivalence where
|
|||
|
|
|
|||
|
|
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 IsEquivalenceInstances where
|
|||
|
|
module ForProd {a} {A B : Set a}
|
|||
|
|
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
|
|||
|
|
(eA : IsEquivalence A _≈₁_) (eB : IsEquivalence B _≈₂_) where
|
|||
|
|
|
|||
|
|
infix 4 _≈_
|
|||
|
|
|
|||
|
|
_≈_ : A × B → A × B → Set a
|
|||
|
|
(a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
|
|||
|
|
|
|||
|
|
ProdEquivalence : IsEquivalence (A × B) _≈_
|
|||
|
|
ProdEquivalence = record
|
|||
|
|
{ ≈-refl = λ {p} →
|
|||
|
|
( IsEquivalence.≈-refl eA
|
|||
|
|
, IsEquivalence.≈-refl eB
|
|||
|
|
)
|
|||
|
|
; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) →
|
|||
|
|
( IsEquivalence.≈-sym eA a₁≈a₂
|
|||
|
|
, IsEquivalence.≈-sym eB b₁≈b₂
|
|||
|
|
)
|
|||
|
|
; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
|
|||
|
|
( IsEquivalence.≈-trans eA a₁≈a₂ a₂≈a₃
|
|||
|
|
, IsEquivalence.≈-trans eB b₁≈b₂ b₂≈b₃
|
|||
|
|
)
|
|||
|
|
}
|