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

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

    module Algebra.Module.Morphism.Construct.Identity where

    open import Algebra.Module.Bundles.Raw
    open import Algebra.Module.Morphism.Structures
      using ( module LeftSemimoduleMorphisms
            ; module LeftModuleMorphisms
            ; module RightSemimoduleMorphisms
            ; module RightModuleMorphisms
            ; module BisemimoduleMorphisms
            ; module BimoduleMorphisms
            ; module SemimoduleMorphisms
            ; module ModuleMorphisms
            )
    open import Algebra.Morphism.Construct.Identity using ( isMonoidHomomorphism; isGroupHomomorphism)
    open import Data.Product.Base using (_,_)
    open import Function.Base using (id)
    import Function.Construct.Identity as Id
    open import Level using (Level)
    open import Relation.Binary.Definitions using (Reflexive)

    private
      variable
        r s m ℓm : Level

    module _ {R : Set r} (M : RawLeftSemimodule R m ℓm) (open RawLeftSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
      open LeftSemimoduleMorphisms M M

      isLeftSemimoduleHomomorphism : IsLeftSemimoduleHomomorphism id
      isLeftSemimoduleHomomorphism = record
        { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism _ ≈ᴹ-refl
        ; *ₗ-homo                 = λ _ _ → ≈ᴹ-refl
        }

      isLeftSemimoduleMonomorphism : IsLeftSemimoduleMonomorphism id
      isLeftSemimoduleMonomorphism = record
        { isLeftSemimoduleHomomorphism = isLeftSemimoduleHomomorphism
        ; injective                    = id
        }

      isLeftSemimoduleIsomorphism : IsLeftSemimoduleIsomorphism id
      isLeftSemimoduleIsomorphism = record
        { isLeftSemimoduleMonomorphism = isLeftSemimoduleMonomorphism
        ; surjective                   = Id.surjective _
        }

    module _ {R : Set r} (M : RawLeftModule R m ℓm) (open RawLeftModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_)  where
      open LeftModuleMorphisms M M

      isLeftModuleHomomorphism : IsLeftModuleHomomorphism id
      isLeftModuleHomomorphism = record
        { +ᴹ-isGroupHomomorphism = isGroupHomomorphism _ ≈ᴹ-refl
        ; *ₗ-homo                = λ _ _ → ≈ᴹ-refl
        }

      isLeftModuleMonomorphism : IsLeftModuleMonomorphism id
      isLeftModuleMonomorphism = record
        { isLeftModuleHomomorphism = isLeftModuleHomomorphism
        ; injective                = id
        }

      isLeftModuleIsomorphism : IsLeftModuleIsomorphism id
      isLeftModuleIsomorphism = record
        { isLeftModuleMonomorphism = isLeftModuleMonomorphism
        ; surjective               = Id.surjective _
        }

    module _ {R : Set r} (M : RawRightSemimodule R m ℓm) (open RawRightSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
      open RightSemimoduleMorphisms M M

      isRightSemimoduleHomomorphism : IsRightSemimoduleHomomorphism id
      isRightSemimoduleHomomorphism = record
        { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism _ ≈ᴹ-refl
        ; *ᵣ-homo                 = λ _ _ → ≈ᴹ-refl
        }

      isRightSemimoduleMonomorphism : IsRightSemimoduleMonomorphism id
      isRightSemimoduleMonomorphism = record
        { isRightSemimoduleHomomorphism = isRightSemimoduleHomomorphism
        ; injective                   = id
        }

      isRightSemimoduleIsomorphism : IsRightSemimoduleIsomorphism id
      isRightSemimoduleIsomorphism = record
        { isRightSemimoduleMonomorphism = isRightSemimoduleMonomorphism
        ; surjective                    = Id.surjective _
        }

    module _ {R : Set r} (M : RawRightModule R m ℓm) (open RawRightModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
      open RightModuleMorphisms M M

      isRightModuleHomomorphism : IsRightModuleHomomorphism id
      isRightModuleHomomorphism = record
        { +ᴹ-isGroupHomomorphism = isGroupHomomorphism _ ≈ᴹ-refl
        ; *ᵣ-homo                = λ _ _ → ≈ᴹ-refl
        }

      isRightModuleMonomorphism : IsRightModuleMonomorphism id
      isRightModuleMonomorphism = record
        { isRightModuleHomomorphism = isRightModuleHomomorphism
        ; injective                 = id
        }

      isRightModuleIsomorphism : IsRightModuleIsomorphism id
      isRightModuleIsomorphism = record
        { isRightModuleMonomorphism = isRightModuleMonomorphism
        ; surjective                = Id.surjective _
        }

    module _ {R : Set r} {S : Set s} (M : RawBisemimodule R S m ℓm) (open RawBisemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
      open BisemimoduleMorphisms M M

      isBisemimoduleHomomorphism : IsBisemimoduleHomomorphism id
      isBisemimoduleHomomorphism = record
        { +ᴹ-isMonoidHomomorphism = isMonoidHomomorphism _ ≈ᴹ-refl
        ; *ₗ-homo                 = λ _ _ → ≈ᴹ-refl
        ; *ᵣ-homo                 = λ _ _ → ≈ᴹ-refl
        }

      isBisemimoduleMonomorphism : IsBisemimoduleMonomorphism id
      isBisemimoduleMonomorphism = record
        { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism
        ; injective                  = id
        }

      isBisemimoduleIsomorphism : IsBisemimoduleIsomorphism id
      isBisemimoduleIsomorphism = record
        { isBisemimoduleMonomorphism = isBisemimoduleMonomorphism
        ; surjective                 = Id.surjective _
        }

    module _ {R : Set r} {S : Set s} (M : RawBimodule R S m ℓm) (open RawBimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
      open BimoduleMorphisms M M

      isBimoduleHomomorphism : IsBimoduleHomomorphism id
      isBimoduleHomomorphism = record
        { +ᴹ-isGroupHomomorphism = isGroupHomomorphism _ ≈ᴹ-refl
        ; *ₗ-homo                = λ _ _ → ≈ᴹ-refl
        ; *ᵣ-homo                = λ _ _ → ≈ᴹ-refl
        }

      isBimoduleMonomorphism : IsBimoduleMonomorphism id
      isBimoduleMonomorphism = record
        { isBimoduleHomomorphism = isBimoduleHomomorphism
        ; injective              = id
        }

      isBimoduleIsomorphism : IsBimoduleIsomorphism id
      isBimoduleIsomorphism = record
        { isBimoduleMonomorphism = isBimoduleMonomorphism
        ; surjective             = Id.surjective _
        }

    module _ {R : Set r} (M : RawSemimodule R m ℓm) (open RawSemimodule M) (≈ᴹ-refl : Reflexive _≈ᴹ_)  where
      open SemimoduleMorphisms M M

      isSemimoduleHomomorphism : IsSemimoduleHomomorphism id
      isSemimoduleHomomorphism = record
        { isBisemimoduleHomomorphism = isBisemimoduleHomomorphism _ ≈ᴹ-refl
        }

      isSemimoduleMonomorphism : IsSemimoduleMonomorphism id
      isSemimoduleMonomorphism = record
        { isSemimoduleHomomorphism = isSemimoduleHomomorphism
        ; injective                = id
        }

      isSemimoduleIsomorphism : IsSemimoduleIsomorphism id
      isSemimoduleIsomorphism = record
        { isSemimoduleMonomorphism = isSemimoduleMonomorphism
        ; surjective               = Id.surjective _
        }

    module _ {R : Set r} (M : RawModule R m ℓm) (open RawModule M) (≈ᴹ-refl : Reflexive _≈ᴹ_) where
      open ModuleMorphisms M M

      isModuleHomomorphism : IsModuleHomomorphism id
      isModuleHomomorphism = record
        { isBimoduleHomomorphism = isBimoduleHomomorphism _ ≈ᴹ-refl
        }

      isModuleMonomorphism : IsModuleMonomorphism id
      isModuleMonomorphism = record
        { isModuleHomomorphism = isModuleHomomorphism
        ; injective            = id
        }

      isModuleIsomorphism : IsModuleIsomorphism id
      isModuleIsomorphism = record
        { isModuleMonomorphism = isModuleMonomorphism
        ; surjective           = Id.surjective _
        }