------------------------------------------------------------------------
-- 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  _⟶ₛ_
_⟶ₛ_ : Setoid a ℓ₁ → Setoid b ℓ₂ → Set _
_⟶ₛ_ = Func

------------------------------------------------------------------------
-- Bundles specialised for propositional equality
------------------------------------------------------------------------

infix  _⟶_ _↣_ _↠_ _⤖_ _⇔_ _↩_ _↪_ _↩↪_ _↔_
_⟶_ : 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  _⟨$⟩_
  _⟨$⟩_ : Func From To → Carrier From → Carrier To
  _⟨$⟩_ = Func.to