    ------------------------------------------------------------------------
    -- 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