------------------------------------------------------------------------ -- The Agda standard library -- -- Some basic properties of bijections. ------------------------------------------------------------------------ {-# OPTIONS --cubical-compatible --safe #-} module Function.Properties.Bijection where open import Function.Bundles open import Level using (Level) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Structures using (IsEquivalence) open import Relation.Binary.Definitions using (Reflexive; Trans) open import Relation.Binary.PropositionalEquality as P using (setoid) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Function.Base using (_∘_) open import Function.Properties.Surjection using (injective⇒to⁻-cong) open import Function.Properties.Inverse using (Inverse⇒Equivalence) import Function.Construct.Identity as Identity import Function.Construct.Symmetry as Symmetry import Function.Construct.Composition as Composition private variable a b c ℓ ℓ₁ ℓ₂ ℓ₃ : Level A B : Set a T S : Setoid a ℓ ------------------------------------------------------------------------ -- Setoid properties refl : Reflexive (Bijection {a} {ℓ}) refl = Identity.bijection _ -- Can't prove full symmetry as we have no proof that the witness -- produced by the surjection proof preserves equality sym-≡ : Bijection S (P.setoid B) → Bijection (P.setoid B) S sym-≡ = Symmetry.bijection-≡ trans : Trans (Bijection {a} {ℓ₁} {b} {ℓ₂}) (Bijection {b} {ℓ₂} {c} {ℓ₃}) Bijection trans = Composition.bijection ------------------------------------------------------------------------ -- Propositional properties ⤖-isEquivalence : IsEquivalence {ℓ = ℓ} _⤖_ ⤖-isEquivalence = record { refl = refl ; sym = sym-≡ ; trans = trans } ------------------------------------------------------------------------ -- Conversion functions Bijection⇒Inverse : Bijection S T → Inverse S T Bijection⇒Inverse bij = record { to = to ; from = to⁻ ; to-cong = cong ; from-cong = injective⇒to⁻-cong surjection injective ; inverse = (λ y≈to⁻[x] → Eq₂.trans (cong y≈to⁻[x]) (to∘to⁻ _)) , (λ y≈to[x] → injective (Eq₂.trans (to∘to⁻ _) y≈to[x])) } where open Bijection bij; to∘to⁻ = proj₂ ∘ strictlySurjective Bijection⇒Equivalence : Bijection T S → Equivalence T S Bijection⇒Equivalence = Inverse⇒Equivalence ∘ Bijection⇒Inverse ⤖⇒↔ : A ⤖ B → A ↔ B ⤖⇒↔ = Bijection⇒Inverse ⤖⇒⇔ : A ⤖ B → A ⇔ B ⤖⇒⇔ = Bijection⇒Equivalence