    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The identity function
    ------------------------------------------------------------------------

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

    module Function.Construct.Identity where

    open import Data.Product.Base using (_,_)
    open import Function.Base using (id)
    open import Function.Bundles
    import Function.Definitions as Definitions
      using (Congruent; Injective; Surjective; Bijective; Inverseʳ; Inverseˡ
            ; Inverseᵇ)
    import Function.Structures as Structures
      using (IsCongruent; IsInjection; IsSurjection; IsBijection; IsLeftInverse
            ; IsRightInverse; IsInverse)
    open import Level using (Level)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Bundles using (Setoid)
    open import Relation.Binary.Structures as B hiding (IsEquivalence)
    open import Relation.Binary.Definitions using (Reflexive)
    open import Relation.Binary.PropositionalEquality.Core using (_≡_)
    open import Relation.Binary.PropositionalEquality.Properties using (setoid)

    private
      variable
        a ℓ : Level
        A : Set a

    ------------------------------------------------------------------------
    -- Properties

    module _ (_≈_ : Rel A ℓ) where

      open Definitions

      congruent : Congruent _≈_ _≈_ id
      congruent = id

      injective : Injective _≈_ _≈_ id
      injective = id

      surjective : Surjective _≈_ _≈_ id
      surjective x = x , id

      bijective : Bijective _≈_ _≈_ id
      bijective = injective , surjective

      inverseˡ : Inverseˡ _≈_ _≈_ id id
      inverseˡ = id

      inverseʳ : Inverseʳ _≈_ _≈_ id id
      inverseʳ = id

      inverseᵇ : Inverseᵇ _≈_ _≈_ id id
      inverseᵇ = inverseˡ , inverseʳ

    ------------------------------------------------------------------------
    -- Structures

    module _ {_≈_ : Rel A ℓ} (isEq : B.IsEquivalence _≈_) where

      open Structures _≈_ _≈_
      open B.IsEquivalence isEq

      isCongruent : IsCongruent id
      isCongruent = record
        { cong           = id
        ; isEquivalence₁ = isEq
        ; isEquivalence₂ = isEq
        }

      isInjection : IsInjection id
      isInjection = record
        { isCongruent = isCongruent
        ; injective   = injective _≈_
        }

      isSurjection : IsSurjection id
      isSurjection = record
        { isCongruent = isCongruent
        ; surjective  = surjective _≈_
        }

      isBijection : IsBijection id
      isBijection = record
        { isInjection = isInjection
        ; surjective  = surjective _≈_
        }

      isLeftInverse : IsLeftInverse id id
      isLeftInverse = record
        { isCongruent = isCongruent
        ; from-cong   = id
        ; inverseˡ    = inverseˡ _≈_
        }

      isRightInverse : IsRightInverse id id
      isRightInverse = record
        { isCongruent = isCongruent
        ; from-cong   = id
        ; inverseʳ    = inverseʳ _≈_
        }

      isInverse : IsInverse id id
      isInverse = record
        { isLeftInverse = isLeftInverse
        ; inverseʳ      = inverseʳ _≈_
        }

    ------------------------------------------------------------------------
    -- Setoid bundles

    module _ (S : Setoid a ℓ) where

      open Setoid S

      function : Func S S
      function = record
        { to   = id
        ; cong = id
        }

      injection : Injection S S
      injection = record
        { to        = id
        ; cong      = id
        ; injective = injective _≈_
        }

      surjection : Surjection S S
      surjection = record
        { to         = id
        ; cong       = id
        ; surjective = surjective _≈_
        }

      bijection : Bijection S S
      bijection = record
        { to        = id
        ; cong      = id
        ; bijective = bijective _≈_
        }

      equivalence : Equivalence S S
      equivalence = record
        { to        = id
        ; from      = id
        ; to-cong   = id
        ; from-cong = id
        }

      leftInverse : LeftInverse S S
      leftInverse = record
        { to        = id
        ; from      = id
        ; to-cong   = id
        ; from-cong = id
        ; inverseˡ  = inverseˡ _≈_
        }

      rightInverse : RightInverse S S
      rightInverse = record
        { to        = id
        ; from      = id
        ; to-cong   = id
        ; from-cong = id
        ; inverseʳ  = inverseʳ _≈_
        }

      inverse : Inverse S S
      inverse = record
        { to        = id
        ; from      = id
        ; to-cong   = id
        ; from-cong = id
        ; inverse   = inverseᵇ _≈_
        }

    ------------------------------------------------------------------------
    -- Propositional bundles

    module _ (A : Set a) where

      ⟶-id : A ⟶ A
      ⟶-id = function (setoid A)

      ↣-id : A ↣ A
      ↣-id = injection (setoid A)

      ↠-id : A ↠ A
      ↠-id = surjection (setoid A)

      ⤖-id : A ⤖ A
      ⤖-id = bijection (setoid A)

      ⇔-id : A ⇔ A
      ⇔-id = equivalence (setoid A)

      ↩-id : A ↩ A
      ↩-id = leftInverse (setoid A)

      ↪-id : A ↪ A
      ↪-id = rightInverse (setoid A)

      ↔-id : A ↔ A
      ↔-id = inverse (setoid A)

    ------------------------------------------------------------------------
    -- DEPRECATED NAMES
    ------------------------------------------------------------------------
    -- Please use the new names as continuing support for the old names is
    -- not guaranteed.

    -- Version v2.0

    id-⟶ = ⟶-id
    {-# WARNING_ON_USAGE id-⟶
    "Warning: id-⟶ was deprecated in v2.0.
    Please use ⟶-id instead."
    #-}

    id-↣ = ↣-id
    {-# WARNING_ON_USAGE id-↣
    "Warning: id-↣ was deprecated in v2.0.
    Please use ↣-id instead."
    #-}

    id-↠ = ↠-id
    {-# WARNING_ON_USAGE id-↠
    "Warning: id-↠ was deprecated in v2.0.
    Please use ↠-id instead."
    #-}

    id-⤖ = ⤖-id
    {-# WARNING_ON_USAGE id-⤖
    "Warning: id-⤖ was deprecated in v2.0.
    Please use ⤖-id instead."
    #-}

    id-⇔ = ⇔-id
    {-# WARNING_ON_USAGE id-⇔
    "Warning: id-⇔ was deprecated in v2.0.
    Please use ⇔-id instead."
    #-}

    id-↩ = ↩-id
    {-# WARNING_ON_USAGE id-↩
    "Warning: id-↩ was deprecated in v2.0.
    Please use ↩-id instead."
    #-}

    id-↪ = ↪-id
    {-# WARNING_ON_USAGE id-↪
    "Warning: id-↪ was deprecated in v2.0.
    Please use ↪-id instead."
    #-}

    id-↔ = ↔-id
    {-# WARNING_ON_USAGE id-↔
    "Warning: id-↔ was deprecated in v2.0.
    Please use ↔-id instead."
    #-}