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

{-# OPTIONS --without-K --safe #-}

module Function.Construct.Identity where

open import Data.Product using (_,_)
open import Function.Base using (id)
open import Function.Bundles
import Function.Definitions as Definitions
import Function.Structures as Structures
open import Level
open import Relation.Binary as B hiding (_⇔_; IsEquivalence)
open import Relation.Binary.PropositionalEquality 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 : Reflexive _≈_ → Surjective id
  surjective refl x = x , refl

  bijective : Reflexive _≈_ → Bijective id
  bijective refl = injective , surjective refl

  inverseˡ : Reflexive _≈_ → Inverseˡ id id
  inverseˡ refl x = refl

  inverseʳ : Reflexive _≈_ → Inverseʳ id id
  inverseʳ refl x = refl

  inverseᵇ : Reflexive _≈_ → Inverseᵇ id id
  inverseᵇ refl = inverseˡ refl , inverseʳ refl

------------------------------------------------------------------------
-- 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 _≈_ refl
    }

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

  isLeftInverse : IsLeftInverse id id
  isLeftInverse = record
    { isCongruent = isCongruent
    ; cong₂       = id
    ; inverseˡ    = inverseˡ _≈_ refl
    }

  isRightInverse : IsRightInverse id id
  isRightInverse = record
    { isCongruent = isCongruent
    ; cong₂       = id
    ; inverseʳ    = inverseʳ _≈_ refl
    }

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

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

module _ (S : Setoid a ℓ) where

  open Setoid S

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

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

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

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

  equivalence : Equivalence S S
  equivalence = record
    { f     = id
    ; g     = id
    ; cong₁ = id
    ; cong₂ = id
    }

  leftInverse : LeftInverse S S
  leftInverse = record
    { f        = id
    ; g        = id
    ; cong₁    = id
    ; cong₂    = id
    ; inverseˡ = inverseˡ _≈_ refl
    }

  rightInverse : RightInverse S S
  rightInverse = record
    { f        = id
    ; g        = id
    ; cong₁    = id
    ; cong₂    = id
    ; inverseʳ = inverseʳ _≈_ refl
    }

  inverse : Inverse S S
  inverse = record
    { f       = id
    ; f⁻¹     = id
    ; cong₁   = id
    ; cong₂   = id
    ; inverse = inverseᵇ _≈_ refl
    }

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