------------------------------------------------------------------------
-- 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."
#-}