------------------------------------------------------------------------ -- The Agda standard library -- -- Bundles for types of functions ------------------------------------------------------------------------ -- The contents of this file should usually be accessed from `Function`. -- Note that these bundles differ from those found elsewhere in other -- library hierarchies as they take Setoids as parameters. This is -- because a function is of no use without knowing what its domain and -- codomain is, as well which equalities are being considered over them. -- One consequence of this is that they are not built from the -- definitions found in `Function.Structures` as is usually the case in -- other library hierarchies, as this would duplicate the equality -- axioms. {-# OPTIONS --cubical-compatible --safe #-} module Function.Bundles where open import Function.Base using (_∘_) open import Function.Definitions import Function.Structures as FunctionStructures open import Level using (Level; _⊔_; suc) open import Data.Product.Base using (_,_; proj₁; proj₂) open import Relation.Binary.Bundles using (Setoid) open import Relation.Binary.Core using (_Preserves_⟶_) open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_) import Relation.Binary.PropositionalEquality.Properties as ≡ open import Function.Consequences.Propositional open Setoid using (isEquivalence) private variable a b ℓ₁ ℓ₂ : Level ------------------------------------------------------------------------ -- Setoid bundles ------------------------------------------------------------------------ module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_) open Setoid To using () renaming (Carrier to B; _≈_ to _≈₂_) open FunctionStructures _≈₁_ _≈₂_ ------------------------------------------------------------------------ -- Bundles with one element -- Called `Func` rather than `Function` in order to avoid clashing -- with the top-level module. record Func : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B cong : Congruent _≈₁_ _≈₂_ to isCongruent : IsCongruent to isCongruent = record { cong = cong ; isEquivalence₁ = isEquivalence From ; isEquivalence₂ = isEquivalence To } open IsCongruent isCongruent public using (module Eq₁; module Eq₂) record Injection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B cong : Congruent _≈₁_ _≈₂_ to injective : Injective _≈₁_ _≈₂_ to function : Func function = record { to = to ; cong = cong } open Func function public hiding (to; cong) isInjection : IsInjection to isInjection = record { isCongruent = isCongruent ; injective = injective } record Surjection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B cong : Congruent _≈₁_ _≈₂_ to surjective : Surjective _≈₁_ _≈₂_ to function : Func function = record { to = to ; cong = cong } open Func function public hiding (to; cong) isSurjection : IsSurjection to isSurjection = record { isCongruent = isCongruent ; surjective = surjective } open IsSurjection isSurjection public using ( strictlySurjective ) to⁻ : B → A to⁻ = proj₁ ∘ surjective to∘to⁻ : ∀ x → to (to⁻ x) ≈₂ x to∘to⁻ = proj₂ ∘ strictlySurjective record Bijection : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B cong : Congruent _≈₁_ _≈₂_ to bijective : Bijective _≈₁_ _≈₂_ to injective : Injective _≈₁_ _≈₂_ to injective = proj₁ bijective surjective : Surjective _≈₁_ _≈₂_ to surjective = proj₂ bijective injection : Injection injection = record { cong = cong ; injective = injective } surjection : Surjection surjection = record { cong = cong ; surjective = surjective } open Injection injection public using (isInjection) open Surjection surjection public using (isSurjection; to⁻; strictlySurjective) isBijection : IsBijection to isBijection = record { isInjection = isInjection ; surjective = surjective } open IsBijection isBijection public using (module Eq₁; module Eq₂) ------------------------------------------------------------------------ -- Bundles with two elements module _ (From : Setoid a ℓ₁) (To : Setoid b ℓ₂) where open Setoid From using () renaming (Carrier to A; _≈_ to _≈₁_) open Setoid To using () renaming (Carrier to B; _≈_ to _≈₂_) open FunctionStructures _≈₁_ _≈₂_ record Equivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B from : B → A to-cong : Congruent _≈₁_ _≈₂_ to from-cong : Congruent _≈₂_ _≈₁_ from toFunction : Func From To toFunction = record { to = to ; cong = to-cong } open Func toFunction public using (module Eq₁; module Eq₂) renaming (isCongruent to to-isCongruent) fromFunction : Func To From fromFunction = record { to = from ; cong = from-cong } open Func fromFunction public using () renaming (isCongruent to from-isCongruent) record LeftInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B from : B → A to-cong : Congruent _≈₁_ _≈₂_ to from-cong : Congruent _≈₂_ _≈₁_ from inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from isCongruent : IsCongruent to isCongruent = record { cong = to-cong ; isEquivalence₁ = isEquivalence From ; isEquivalence₂ = isEquivalence To } isLeftInverse : IsLeftInverse to from isLeftInverse = record { isCongruent = isCongruent ; from-cong = from-cong ; inverseˡ = inverseˡ } open IsLeftInverse isLeftInverse public using (module Eq₁; module Eq₂; strictlyInverseˡ; isSurjection) equivalence : Equivalence equivalence = record { to-cong = to-cong ; from-cong = from-cong } isSplitSurjection : IsSplitSurjection to isSplitSurjection = record { from = from ; isLeftInverse = isLeftInverse } surjection : Surjection From To surjection = record { to = to ; cong = to-cong ; surjective = λ y → from y , inverseˡ } record RightInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B from : B → A to-cong : Congruent _≈₁_ _≈₂_ to from-cong : from Preserves _≈₂_ ⟶ _≈₁_ inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from isCongruent : IsCongruent to isCongruent = record { cong = to-cong ; isEquivalence₁ = isEquivalence From ; isEquivalence₂ = isEquivalence To } isRightInverse : IsRightInverse to from isRightInverse = record { isCongruent = isCongruent ; from-cong = from-cong ; inverseʳ = inverseʳ } open IsRightInverse isRightInverse public using (module Eq₁; module Eq₂; strictlyInverseʳ) equivalence : Equivalence equivalence = record { to-cong = to-cong ; from-cong = from-cong } record Inverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B from : B → A to-cong : Congruent _≈₁_ _≈₂_ to from-cong : Congruent _≈₂_ _≈₁_ from inverse : Inverseᵇ _≈₁_ _≈₂_ to from inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from inverseˡ = proj₁ inverse inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from inverseʳ = proj₂ inverse leftInverse : LeftInverse leftInverse = record { to-cong = to-cong ; from-cong = from-cong ; inverseˡ = inverseˡ } rightInverse : RightInverse rightInverse = record { to-cong = to-cong ; from-cong = from-cong ; inverseʳ = inverseʳ } open LeftInverse leftInverse public using (isLeftInverse; strictlyInverseˡ) open RightInverse rightInverse public using (isRightInverse; strictlyInverseʳ) isInverse : IsInverse to from isInverse = record { isLeftInverse = isLeftInverse ; inverseʳ = inverseʳ } open IsInverse isInverse public using (module Eq₁; module Eq₂) ------------------------------------------------------------------------ -- Bundles with three elements record BiEquivalence : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B from₁ : B → A from₂ : B → A to-cong : Congruent _≈₁_ _≈₂_ to from₁-cong : Congruent _≈₂_ _≈₁_ from₁ from₂-cong : Congruent _≈₂_ _≈₁_ from₂ record BiInverse : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where field to : A → B from₁ : B → A from₂ : B → A to-cong : Congruent _≈₁_ _≈₂_ to from₁-cong : Congruent _≈₂_ _≈₁_ from₁ from₂-cong : Congruent _≈₂_ _≈₁_ from₂ inverseˡ : Inverseˡ _≈₁_ _≈₂_ to from₁ inverseʳ : Inverseʳ _≈₁_ _≈₂_ to from₂ to-isCongruent : IsCongruent to to-isCongruent = record { cong = to-cong ; isEquivalence₁ = isEquivalence From ; isEquivalence₂ = isEquivalence To } isBiInverse : IsBiInverse to from₁ from₂ isBiInverse = record { to-isCongruent = to-isCongruent ; from₁-cong = from₁-cong ; from₂-cong = from₂-cong ; inverseˡ = inverseˡ ; inverseʳ = inverseʳ } biEquivalence : BiEquivalence biEquivalence = record { to-cong = to-cong ; from₁-cong = from₁-cong ; from₂-cong = from₂-cong } ------------------------------------------------------------------------ -- Other -- A left inverse is also known as a “split surjection”. -- -- As the name implies, a split surjection is a special kind of -- surjection where the witness generated in the domain in the -- function for elements `x₁` and `x₂` are equal if `x₁ ≈ x₂` . -- -- The difference is the `from-cong` law --- generally, the section -- (called `Surjection.to⁻` or `SplitSurjection.from`) of a surjection -- need not respect equality, whereas it must in a split surjection. -- -- The two notions coincide when the equivalence relation on `B` is -- propositional equality (because all functions respect propositional -- equality). -- -- For further background on (split) surjections, one may consult any -- general mathematical references which work without the principle -- of choice. For example: -- -- https://ncatlab.org/nlab/show/split+epimorphism. -- -- The connection to set-theoretic notions with the same names is -- justified by the setoid type theory/homotopy type theory -- observation/definition that (∃x : A. P) = ∥ Σx : A. P ∥ --- i.e., -- we can read set-theoretic ∃ as squashed/propositionally truncated Σ. -- -- We see working with setoids as working in the MLTT model of a setoid -- type theory, in which ∥ X ∥ is interpreted as the setoid with carrier -- set X and the equivalence relation that relates all elements. -- All maps into ∥ X ∥ respect equality, so in the idiomatic definitions -- here, we drop the corresponding trivial `cong` field completely. SplitSurjection : Set _ SplitSurjection = LeftInverse module SplitSurjection (splitSurjection : SplitSurjection) = LeftInverse splitSurjection ------------------------------------------------------------------------ -- Infix abbreviations for oft-used items ------------------------------------------------------------------------ -- Same naming convention as used for propositional equality below, with -- appended ₛ (for 'S'etoid). infixr 0 _⟶ₛ_ _⟶ₛ_ : Setoid a ℓ₁ → Setoid b ℓ₂ → Set _ _⟶ₛ_ = Func ------------------------------------------------------------------------ -- Bundles specialised for propositional equality ------------------------------------------------------------------------ infix 3 _⟶_ _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_ _⟶_ : Set a → Set b → Set _ A ⟶ B = Func (≡.setoid A) (≡.setoid B) _↣_ : Set a → Set b → Set _ A ↣ B = Injection (≡.setoid A) (≡.setoid B) _↠_ : Set a → Set b → Set _ A ↠ B = Surjection (≡.setoid A) (≡.setoid B) _⤖_ : Set a → Set b → Set _ A ⤖ B = Bijection (≡.setoid A) (≡.setoid B) _⇔_ : Set a → Set b → Set _ A ⇔ B = Equivalence (≡.setoid A) (≡.setoid B) _↩_ : Set a → Set b → Set _ A ↩ B = LeftInverse (≡.setoid A) (≡.setoid B) _↪_ : Set a → Set b → Set _ A ↪ B = RightInverse (≡.setoid A) (≡.setoid B) _↩↪_ : Set a → Set b → Set _ A ↩↪ B = BiInverse (≡.setoid A) (≡.setoid B) _↔_ : Set a → Set b → Set _ A ↔ B = Inverse (≡.setoid A) (≡.setoid B) -- We now define some constructors for the above that -- automatically provide the required congruency proofs. module _ {A : Set a} {B : Set b} where mk⟶ : (A → B) → A ⟶ B mk⟶ to = record { to = to ; cong = ≡.cong to } mk↣ : ∀ {to : A → B} → Injective _≡_ _≡_ to → A ↣ B mk↣ {to} inj = record { to = to ; cong = ≡.cong to ; injective = inj } mk↠ : ∀ {to : A → B} → Surjective _≡_ _≡_ to → A ↠ B mk↠ {to} surj = record { to = to ; cong = ≡.cong to ; surjective = surj } mk⤖ : ∀ {to : A → B} → Bijective _≡_ _≡_ to → A ⤖ B mk⤖ {to} bij = record { to = to ; cong = ≡.cong to ; bijective = bij } mk⇔ : ∀ (to : A → B) (from : B → A) → A ⇔ B mk⇔ to from = record { to = to ; from = from ; to-cong = ≡.cong to ; from-cong = ≡.cong from } mk↩ : ∀ {to : A → B} {from : B → A} → Inverseˡ _≡_ _≡_ to from → A ↩ B mk↩ {to} {from} invˡ = record { to = to ; from = from ; to-cong = ≡.cong to ; from-cong = ≡.cong from ; inverseˡ = invˡ } mk↪ : ∀ {to : A → B} {from : B → A} → Inverseʳ _≡_ _≡_ to from → A ↪ B mk↪ {to} {from} invʳ = record { to = to ; from = from ; to-cong = ≡.cong to ; from-cong = ≡.cong from ; inverseʳ = invʳ } mk↩↪ : ∀ {to : A → B} {from₁ : B → A} {from₂ : B → A} → Inverseˡ _≡_ _≡_ to from₁ → Inverseʳ _≡_ _≡_ to from₂ → A ↩↪ B mk↩↪ {to} {from₁} {from₂} invˡ invʳ = record { to = to ; from₁ = from₁ ; from₂ = from₂ ; to-cong = ≡.cong to ; from₁-cong = ≡.cong from₁ ; from₂-cong = ≡.cong from₂ ; inverseˡ = invˡ ; inverseʳ = invʳ } mk↔ : ∀ {to : A → B} {from : B → A} → Inverseᵇ _≡_ _≡_ to from → A ↔ B mk↔ {to} {from} inv = record { to = to ; from = from ; to-cong = ≡.cong to ; from-cong = ≡.cong from ; inverse = inv } -- Strict variant of the above. mk↠ₛ : ∀ {to : A → B} → StrictlySurjective _≡_ to → A ↠ B mk↠ₛ = mk↠ ∘ strictlySurjective⇒surjective mk↔ₛ′ : ∀ (to : A → B) (from : B → A) → StrictlyInverseˡ _≡_ to from → StrictlyInverseʳ _≡_ to from → A ↔ B mk↔ₛ′ to from invˡ invʳ = mk↔ {to} {from} ( strictlyInverseˡ⇒inverseˡ to invˡ , strictlyInverseʳ⇒inverseʳ to invʳ ) ------------------------------------------------------------------------ -- Other ------------------------------------------------------------------------ -- Alternative syntax for the application of functions module _ {From : Setoid a ℓ₁} {To : Setoid b ℓ₂} where open Setoid infixl 5 _⟨$⟩_ _⟨$⟩_ : Func From To → Carrier From → Carrier To _⟨$⟩_ = Func.to