    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- The identity morphism for algebraic structures
    ------------------------------------------------------------------------

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

    module Algebra.Morphism.Construct.Identity where

    open import Algebra.Bundles
    open import Algebra.Morphism.Bundles
    open import Algebra.Morphism.Structures
      using ( module MagmaMorphisms
            ; module MonoidMorphisms
            ; module GroupMorphisms
            ; module NearSemiringMorphisms
            ; module SemiringMorphisms
            ; module RingWithoutOneMorphisms
            ; module RingMorphisms
            ; module QuasigroupMorphisms
            ; module LoopMorphisms
            ; module KleeneAlgebraMorphisms
            )
    open import Function.Base using (id)
    import Function.Construct.Identity as Id
    open import Level using (Level)
    open import Relation.Binary.Morphism.Construct.Identity using (isRelHomomorphism)
    open import Relation.Binary.Definitions using (Reflexive)

    private
      variable
        c ℓ : Level

    ------------------------------------------------------------------------
    -- Magmas

    module _ (M : RawMagma c ℓ) (open RawMagma M) (refl : Reflexive _≈_) where
      open MagmaMorphisms M M

      isMagmaHomomorphism : IsMagmaHomomorphism id
      isMagmaHomomorphism = record
        { isRelHomomorphism = isRelHomomorphism _
        ; homo              = λ _ _ → refl
        }

      isMagmaMonomorphism : IsMagmaMonomorphism id
      isMagmaMonomorphism = record
        { isMagmaHomomorphism = isMagmaHomomorphism
        ; injective = id
        }

      isMagmaIsomorphism : IsMagmaIsomorphism id
      isMagmaIsomorphism = record
        { isMagmaMonomorphism = isMagmaMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- Monoids

    module _ (M : RawMonoid c ℓ) (open RawMonoid M) (refl : Reflexive _≈_) where
      open MonoidMorphisms M M

      isMonoidHomomorphism : IsMonoidHomomorphism id
      isMonoidHomomorphism = record
        { isMagmaHomomorphism = isMagmaHomomorphism _ refl
        ; ε-homo = refl
        }

      isMonoidMonomorphism : IsMonoidMonomorphism id
      isMonoidMonomorphism = record
        { isMonoidHomomorphism = isMonoidHomomorphism
        ; injective = id
        }

      isMonoidIsomorphism : IsMonoidIsomorphism id
      isMonoidIsomorphism = record
        { isMonoidMonomorphism = isMonoidMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- Groups

    module _ (G : RawGroup c ℓ) (open RawGroup G) (refl : Reflexive _≈_) where
      open GroupMorphisms G G

      isGroupHomomorphism : IsGroupHomomorphism id
      isGroupHomomorphism = record
        { isMonoidHomomorphism = isMonoidHomomorphism _ refl
        ; ⁻¹-homo = λ _ → refl
        }

      isGroupMonomorphism : IsGroupMonomorphism id
      isGroupMonomorphism = record
        { isGroupHomomorphism = isGroupHomomorphism
        ; injective = id
        }

      isGroupIsomorphism : IsGroupIsomorphism id
      isGroupIsomorphism = record
        { isGroupMonomorphism = isGroupMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- Near semirings

    module _ (R : RawNearSemiring c ℓ) (open RawNearSemiring R) (refl : Reflexive _≈_) where
      open NearSemiringMorphisms R R

      isNearSemiringHomomorphism : IsNearSemiringHomomorphism id
      isNearSemiringHomomorphism = record
        { +-isMonoidHomomorphism = isMonoidHomomorphism _ refl
        ; *-homo                 = λ _ _ → refl
        }

      isNearSemiringMonomorphism : IsNearSemiringMonomorphism id
      isNearSemiringMonomorphism = record
        { isNearSemiringHomomorphism = isNearSemiringHomomorphism
        ; injective = id
        }

      isNearSemiringIsomorphism : IsNearSemiringIsomorphism id
      isNearSemiringIsomorphism = record
        { isNearSemiringMonomorphism = isNearSemiringMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- Semirings

    module _ (R : RawSemiring c ℓ) (open RawSemiring R) (refl : Reflexive _≈_) where
      open SemiringMorphisms R R

      isSemiringHomomorphism : IsSemiringHomomorphism id
      isSemiringHomomorphism = record
        { isNearSemiringHomomorphism = isNearSemiringHomomorphism _ refl
        ; 1#-homo                    = refl
        }

      isSemiringMonomorphism : IsSemiringMonomorphism id
      isSemiringMonomorphism = record
        { isSemiringHomomorphism = isSemiringHomomorphism
        ; injective = id
        }

      isSemiringIsomorphism : IsSemiringIsomorphism id
      isSemiringIsomorphism = record
        { isSemiringMonomorphism = isSemiringMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- RingWithoutOne

    module _ (R : RawRingWithoutOne c ℓ) (open RawRingWithoutOne R) (refl : Reflexive _≈_) where
      open RingWithoutOneMorphisms R R

      isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism id
      isRingWithoutOneHomomorphism = record
        { +-isGroupHomomorphism  = isGroupHomomorphism _ refl
        ; *-homo                 = λ _ _ → refl
        }

      isRingWithoutOneMonomorphism : IsRingWithoutOneMonomorphism id
      isRingWithoutOneMonomorphism = record
        { isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism
        ; injective = id
        }

      isRingWithoutOneIsoMorphism : IsRingWithoutOneIsoMorphism id
      isRingWithoutOneIsoMorphism = record
        { isRingWithoutOneMonomorphism = isRingWithoutOneMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- Rings

    module _ (R : RawRing c ℓ) (open RawRing R) (refl : Reflexive _≈_) where
      open RingMorphisms R R

      isRingHomomorphism : IsRingHomomorphism id
      isRingHomomorphism = record
        { isSemiringHomomorphism = isSemiringHomomorphism _ refl
        ; -‿homo                 = λ _ → refl
        }

      isRingMonomorphism : IsRingMonomorphism id
      isRingMonomorphism = record
        { isRingHomomorphism = isRingHomomorphism
        ; injective = id
        }

      isRingIsomorphism : IsRingIsomorphism id
      isRingIsomorphism = record
        { isRingMonomorphism = isRingMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- Quasigroup

    module _ (Q : RawQuasigroup c ℓ) (open RawQuasigroup Q) (refl : Reflexive _≈_) where
      open QuasigroupMorphisms Q Q

      isQuasigroupHomomorphism : IsQuasigroupHomomorphism id
      isQuasigroupHomomorphism = record
        { isRelHomomorphism = isRelHomomorphism _
        ; ∙-homo            = λ _ _ → refl
        ; \\-homo            = λ _ _ → refl
        ; //-homo            = λ _ _ → refl
        }

      isQuasigroupMonomorphism : IsQuasigroupMonomorphism id
      isQuasigroupMonomorphism = record
        { isQuasigroupHomomorphism = isQuasigroupHomomorphism
        ; injective = id
        }

      isQuasigroupIsomorphism : IsQuasigroupIsomorphism id
      isQuasigroupIsomorphism = record
        { isQuasigroupMonomorphism = isQuasigroupMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- Loop

    module _ (L : RawLoop c ℓ) (open RawLoop L) (refl : Reflexive _≈_) where
      open LoopMorphisms L L

      isLoopHomomorphism : IsLoopHomomorphism id
      isLoopHomomorphism = record
        { isQuasigroupHomomorphism = isQuasigroupHomomorphism _ refl
        ; ε-homo = refl
        }

      isLoopMonomorphism : IsLoopMonomorphism id
      isLoopMonomorphism = record
        { isLoopHomomorphism = isLoopHomomorphism
        ; injective = id
        }

      isLoopIsomorphism : IsLoopIsomorphism id
      isLoopIsomorphism = record
        { isLoopMonomorphism = isLoopMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    -- KleeneAlgebra

    module _ (K : RawKleeneAlgebra c ℓ) (open RawKleeneAlgebra K) (refl : Reflexive _≈_) where
      open KleeneAlgebraMorphisms K K

      isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism id
      isKleeneAlgebraHomomorphism = record
        { isSemiringHomomorphism = isSemiringHomomorphism _ refl
        ; ⋆-homo = λ _ → refl
        }

      isKleeneAlgebraMonomorphism : IsKleeneAlgebraMonomorphism id
      isKleeneAlgebraMonomorphism = record
        { isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism
        ; injective = id
        }

      isKleeneAlgebraIsomorphism : IsKleeneAlgebraIsomorphism id
      isKleeneAlgebraIsomorphism = record
        { isKleeneAlgebraMonomorphism = isKleeneAlgebraMonomorphism
        ; surjective = Id.surjective _
        }

    ------------------------------------------------------------------------
    --- Bundled morphisms between algebras
    -----------------------------------------------------------------------

    -- Magma

    module _ (M : Magma c ℓ) where

      open Magma M using (rawMagma; refl)
      open MagmaMorphisms rawMagma rawMagma

      magmaHomomorphism : MagmaHomomorphism rawMagma rawMagma
      magmaHomomorphism = record
        { ⟦_⟧ = id
        ; isMagmaHomomorphism = isMagmaHomomorphism rawMagma refl
        }

    -- Monoid

    module _ (M : Monoid c ℓ) where

      open Monoid M using (rawMonoid; refl)
      open MonoidMorphisms rawMonoid rawMonoid

      monoidHomomorphism : MonoidHomomorphism rawMonoid rawMonoid
      monoidHomomorphism = record
        { ⟦_⟧ = id
        ; isMonoidHomomorphism = isMonoidHomomorphism rawMonoid refl
        }

    -- Group

    module _ (M : Group c ℓ) where

      open Group M using (rawGroup; refl)
      open GroupMorphisms rawGroup rawGroup

      groupHomomorphism : GroupHomomorphism rawGroup rawGroup
      groupHomomorphism = record
        { ⟦_⟧ = id
        ; isGroupHomomorphism = isGroupHomomorphism rawGroup refl
        }

    -- NearSemiring

    module _ (M : NearSemiring c ℓ) where

      open NearSemiring M using (rawNearSemiring; refl)
      open NearSemiringMorphisms rawNearSemiring rawNearSemiring

      nearSemiringHomomorphism : NearSemiringHomomorphism rawNearSemiring rawNearSemiring
      nearSemiringHomomorphism = record
        { ⟦_⟧ = id
        ; isNearSemiringHomomorphism = isNearSemiringHomomorphism rawNearSemiring refl
        }

    -- Semiring

    module _ (M : Semiring c ℓ) where

      open Semiring M using (rawSemiring; refl)
      open SemiringMorphisms rawSemiring rawSemiring

      semiringHomomorphism : SemiringHomomorphism rawSemiring rawSemiring
      semiringHomomorphism = record
        { ⟦_⟧ = id
        ; isSemiringHomomorphism = isSemiringHomomorphism rawSemiring refl
        }

    -- KleeneAlgebra

    module _ (M : KleeneAlgebra c ℓ) where

      open KleeneAlgebra M using (rawKleeneAlgebra; refl)
      open KleeneAlgebraMorphisms rawKleeneAlgebra rawKleeneAlgebra

      kleeneAlgebraHomomorphism : KleeneAlgebraHomomorphism rawKleeneAlgebra rawKleeneAlgebra
      kleeneAlgebraHomomorphism = record
        { ⟦_⟧ = id
        ; isKleeneAlgebraHomomorphism = isKleeneAlgebraHomomorphism rawKleeneAlgebra refl
        }

    -- RingWithoutOne

    module _ (M : RingWithoutOne c ℓ) where

      open RingWithoutOne M using (rawRingWithoutOne; refl)
      open RingWithoutOneMorphisms rawRingWithoutOne rawRingWithoutOne

      ringWithoutOneHomomorphism : RingWithoutOneHomomorphism rawRingWithoutOne rawRingWithoutOne
      ringWithoutOneHomomorphism = record
        { ⟦_⟧ = id
        ; isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism rawRingWithoutOne refl
        }

    -- Ring

    module _ (M : Ring c ℓ) where

      open Ring M using (rawRing; refl)
      open RingMorphisms rawRing rawRing

      ringHomomorphism : RingHomomorphism rawRing rawRing
      ringHomomorphism = record
        { ⟦_⟧ = id
        ; isRingHomomorphism = isRingHomomorphism rawRing refl
        }

    -- Quasigroup

    module _ (M : Quasigroup c ℓ) where

      open Quasigroup M using (rawQuasigroup; refl)
      open QuasigroupMorphisms rawQuasigroup rawQuasigroup

      quasigroupHomomorphism : QuasigroupHomomorphism rawQuasigroup rawQuasigroup
      quasigroupHomomorphism = record
        { ⟦_⟧ = id
        ; isQuasigroupHomomorphism = isQuasigroupHomomorphism rawQuasigroup refl
        }

    -- Loop

    module _ (M : Loop c ℓ) where

      open Loop M using (rawLoop; refl)
      open LoopMorphisms rawLoop rawLoop

      loopHomomorphism : LoopHomomorphism rawLoop rawLoop
      loopHomomorphism = record
        { ⟦_⟧ = id
        ; isLoopHomomorphism = isLoopHomomorphism rawLoop refl
        }