{-# OPTIONS --universe-polymorphism #-}
module Function.Equivalence where
open import Function using (flip)
open import Function.Equality as F
using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_)
open import Level
open import Relation.Binary
import Relation.Binary.PropositionalEquality as P
record Equivalent {f₁ f₂ t₁ t₂}
(From : Setoid f₁ f₂) (To : Setoid t₁ t₂) :
Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
field
to : From ⟶ To
from : To ⟶ From
infix 3 _⇔_
_⇔_ : ∀ {f t} → Set f → Set t → Set _
From ⇔ To = Equivalent (P.setoid From) (P.setoid To)
equivalent : ∀ {f t} {From : Set f} {To : Set t} →
(From → To) → (To → From) → From ⇔ To
equivalent to from = record { to = P.→-to-⟶ to; from = P.→-to-⟶ from }
id : ∀ {s₁ s₂} → Reflexive (Equivalent {s₁} {s₂})
id {x = S} = record
{ to = F.id
; from = F.id
}
infixr 9 _∘_
_∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂} →
TransFlip (Equivalent {f₁} {f₂} {m₁} {m₂})
(Equivalent {m₁} {m₂} {t₁} {t₂})
(Equivalent {f₁} {f₂} {t₁} {t₂})
f ∘ g = record
{ to = to f ⟪∘⟫ to g
; from = from g ⟪∘⟫ from f
} where open Equivalent
sym : ∀ {f₁ f₂ t₁ t₂} →
Sym (Equivalent {f₁} {f₂} {t₁} {t₂}) (Equivalent {t₁} {t₂} {f₁} {f₂})
sym eq = record
{ from = to
; to = from
} where open Equivalent eq
InducedEquivalence₁ : ∀ {a s₁ s₂} {A : Set a}
(S : A → Setoid s₁ s₂) → Setoid _ _
InducedEquivalence₁ S = record
{ _≈_ = λ x y → Equivalent (S x) (S y)
; isEquivalence = record
{ refl = id
; sym = sym
; trans = flip _∘_
}
}
InducedEquivalence₂ : ∀ {a b s₁ s₂} {A : Set a} {B : Set b}
(_S_ : A → B → Setoid s₁ s₂) → Setoid _ _
InducedEquivalence₂ _S_ = record
{ _≈_ = λ x y → ∀ {z} → Equivalent (z S x) (z S y)
; isEquivalence = record
{ refl = id
; sym = λ i≈j → sym i≈j
; trans = λ i≈j j≈k → j≈k ∘ i≈j
}
}