------------------------------------------------------------------------ -- The Agda standard library -- -- Equivalence (coinhabitance) ------------------------------------------------------------------------ {-# OPTIONS --without-K --safe #-} module Function.Equivalence where -- Note: use of the standard function hierarchy is encouraged. The -- module `Function` re-exports `Congruent` and `IsCongruent`. -- The alternative definitions found in this file will eventually be -- deprecated. open import Function.Base using (flip) open import Function.Equality as F using (_⟶_; _⟨$⟩_) renaming (_∘_ to _⟪∘⟫_) open import Level open import Relation.Binary hiding (_⇔_) import Relation.Binary.PropositionalEquality as P ------------------------------------------------------------------------ -- Setoid equivalence record Equivalence {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 ------------------------------------------------------------------------ -- The set of all equivalences between two sets (i.e. equivalences -- with propositional equality) infix 3 _⇔_ _⇔_ : ∀ {f t} → Set f → Set t → Set _ From ⇔ To = Equivalence (P.setoid From) (P.setoid To) equivalence : ∀ {f t} {From : Set f} {To : Set t} → (From → To) → (To → From) → From ⇔ To equivalence to from = record { to = P.→-to-⟶ to ; from = P.→-to-⟶ from } ------------------------------------------------------------------------ -- Equivalence is an equivalence relation -- Identity and composition (reflexivity and transitivity). id : ∀ {s₁ s₂} → Reflexive (Equivalence {s₁} {s₂}) id {x = S} = record { to = F.id ; from = F.id } infixr 9 _∘_ _∘_ : ∀ {f₁ f₂ m₁ m₂ t₁ t₂} → TransFlip (Equivalence {f₁} {f₂} {m₁} {m₂}) (Equivalence {m₁} {m₂} {t₁} {t₂}) (Equivalence {f₁} {f₂} {t₁} {t₂}) f ∘ g = record { to = to f ⟪∘⟫ to g ; from = from g ⟪∘⟫ from f } where open Equivalence -- Symmetry. sym : ∀ {f₁ f₂ t₁ t₂} → Sym (Equivalence {f₁} {f₂} {t₁} {t₂}) (Equivalence {t₁} {t₂} {f₁} {f₂}) sym eq = record { from = to ; to = from } where open Equivalence eq -- For fixed universe levels we can construct setoids. setoid : (s₁ s₂ : Level) → Setoid (suc (s₁ ⊔ s₂)) (s₁ ⊔ s₂) setoid s₁ s₂ = record { Carrier = Setoid s₁ s₂ ; _≈_ = Equivalence ; isEquivalence = record { refl = id ; sym = sym ; trans = flip _∘_ } } ⇔-setoid : (ℓ : Level) → Setoid (suc ℓ) ℓ ⇔-setoid ℓ = record { Carrier = Set ℓ ; _≈_ = _⇔_ ; isEquivalence = record { refl = id ; sym = sym ; trans = flip _∘_ } } ------------------------------------------------------------------------ -- Transformations map : ∀ {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} {f₁′ f₂′ t₁′ t₂′} {From′ : Setoid f₁′ f₂′} {To′ : Setoid t₁′ t₂′} → ((From ⟶ To) → (From′ ⟶ To′)) → ((To ⟶ From) → (To′ ⟶ From′)) → Equivalence From To → Equivalence From′ To′ map t f eq = record { to = t to; from = f from } where open Equivalence eq zip : ∀ {f₁₁ f₂₁ t₁₁ t₂₁} {From₁ : Setoid f₁₁ f₂₁} {To₁ : Setoid t₁₁ t₂₁} {f₁₂ f₂₂ t₁₂ t₂₂} {From₂ : Setoid f₁₂ f₂₂} {To₂ : Setoid t₁₂ t₂₂} {f₁ f₂ t₁ t₂} {From : Setoid f₁ f₂} {To : Setoid t₁ t₂} → ((From₁ ⟶ To₁) → (From₂ ⟶ To₂) → (From ⟶ To)) → ((To₁ ⟶ From₁) → (To₂ ⟶ From₂) → (To ⟶ From)) → Equivalence From₁ To₁ → Equivalence From₂ To₂ → Equivalence From To zip t f eq₁ eq₂ = record { to = t (to eq₁) (to eq₂); from = f (from eq₁) (from eq₂) } where open Equivalence