    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Structures for types of functions
    ------------------------------------------------------------------------

    -- The contents of this file should usually be accessed from `Function`.

    {-# OPTIONS --cubical-compatible --safe #-}

    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Structures using (IsEquivalence)

    module Function.Structures {a b ℓ₁ ℓ₂}
      {A : Set a} (_≈₁_ : Rel A ℓ₁) -- Equality over the domain
      {B : Set b} (_≈₂_ : Rel B ℓ₂) -- Equality over the codomain
      where

    open import Data.Product.Base as Product using (∃; _×_; _,_)
    open import Function.Base
    open import Function.Definitions
    open import Level using (_⊔_)

    ------------------------------------------------------------------------
    -- One element structures
    ------------------------------------------------------------------------

    record IsCongruent (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        cong           : Congruent _≈₁_ _≈₂_ to
        isEquivalence₁ : IsEquivalence _≈₁_
        isEquivalence₂ : IsEquivalence _≈₂_

      module Eq₁ where

        setoid : Setoid a ℓ₁
        setoid = record
          { isEquivalence = isEquivalence₁
          }

        open Setoid setoid public

      module Eq₂ where

        setoid : Setoid b ℓ₂
        setoid = record
          { isEquivalence = isEquivalence₂
          }

        open Setoid setoid public

    record IsInjection (to : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        isCongruent : IsCongruent to
        injective   : Injective _≈₁_ _≈₂_ to

      open IsCongruent isCongruent public

    record IsSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        isCongruent : IsCongruent f
        surjective  : Surjective _≈₁_ _≈₂_ f

      open IsCongruent isCongruent public

      strictlySurjective : StrictlySurjective _≈₂_ f
      strictlySurjective x = Product.map₂ (λ v → v Eq₁.refl) (surjective x)

    record IsBijection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        isInjection : IsInjection f
        surjective  : Surjective _≈₁_ _≈₂_ f

      open IsInjection isInjection public

      bijective : Bijective _≈₁_ _≈₂_ f
      bijective = injective , surjective

      isSurjection : IsSurjection f
      isSurjection = record
        { isCongruent = isCongruent
        ; surjective  = surjective
        }

      open IsSurjection isSurjection public
        using (strictlySurjective)

    ------------------------------------------------------------------------
    -- Two element structures
    ------------------------------------------------------------------------

    record IsLeftInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        isCongruent  : IsCongruent to
        from-cong    : Congruent _≈₂_ _≈₁_ from
        inverseˡ     : Inverseˡ _≈₁_ _≈₂_ to from

      open IsCongruent isCongruent public
        renaming (cong to to-cong)

      strictlyInverseˡ : StrictlyInverseˡ _≈₂_ to from
      strictlyInverseˡ x = inverseˡ Eq₁.refl

      isSurjection : IsSurjection to
      isSurjection = record
        { isCongruent = isCongruent
        ; surjective = λ y → from y , inverseˡ
        }

    record IsRightInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        isCongruent : IsCongruent to
        from-cong   : Congruent _≈₂_ _≈₁_ from
        inverseʳ    : Inverseʳ _≈₁_ _≈₂_ to from

      open IsCongruent isCongruent public
        renaming (cong to to-cong)

      strictlyInverseʳ : StrictlyInverseʳ _≈₁_ to from
      strictlyInverseʳ x = inverseʳ Eq₂.refl

    record IsInverse (to : A → B) (from : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        isLeftInverse : IsLeftInverse to from
        inverseʳ      : Inverseʳ _≈₁_ _≈₂_ to from

      open IsLeftInverse isLeftInverse public

      isRightInverse : IsRightInverse to from
      isRightInverse = record
        { isCongruent = isCongruent
        ; from-cong   = from-cong
        ; inverseʳ    = inverseʳ
        }

      open IsRightInverse isRightInverse public
        using (strictlyInverseʳ)

      inverse : Inverseᵇ _≈₁_ _≈₂_ to from
      inverse = inverseˡ , inverseʳ

    ------------------------------------------------------------------------
    -- Three element structures
    ------------------------------------------------------------------------

    record IsBiEquivalence
      (to : A → B) (from₁ : B → A) (from₂ : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        to-isCongruent : IsCongruent to
        from₁-cong    : Congruent _≈₂_ _≈₁_ from₁
        from₂-cong    : Congruent _≈₂_ _≈₁_ from₂

      open IsCongruent to-isCongruent public
        renaming (cong to to-cong₁)

    record IsBiInverse
      (to : A → B) (from₁ : B → A) (from₂ : B → A) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        to-isCongruent : IsCongruent to
        from₁-cong     : Congruent _≈₂_ _≈₁_ from₁
        from₂-cong     : Congruent _≈₂_ _≈₁_ from₂
        inverseˡ       : Inverseˡ _≈₁_ _≈₂_ to from₁
        inverseʳ       : Inverseʳ _≈₁_ _≈₂_ to from₂

      open IsCongruent to-isCongruent public
        renaming (cong to to-cong)

    ------------------------------------------------------------------------
    -- Other
    ------------------------------------------------------------------------

    -- See the comment on `SplitSurjection` in `Function.Bundles` for an
    -- explanation of (split) surjections.
    record IsSplitSurjection (f : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
      field
        from : B → A
        isLeftInverse : IsLeftInverse f from

      open IsLeftInverse isLeftInverse public