    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Morphisms between algebraic structures
    ------------------------------------------------------------------------

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

    module Algebra.Morphism.Structures where

    open import Algebra.Core using (Op₁; Op₂)
    open import Algebra.Bundles
    import Algebra.Morphism.Definitions as MorphismDefinitions
    open import Level using (Level; _⊔_)
    open import Function.Definitions using (Injective; Surjective)
    open import Relation.Binary.Core using (Rel)
    open import Relation.Binary.Morphism.Structures
      using (IsRelHomomorphism; IsRelMonomorphism; IsRelIsomorphism)

    private
      variable
        a b ℓ₁ ℓ₂ : Level

    ------------------------------------------------------------------------
    -- Morphisms over SuccessorSet-like structures
    ------------------------------------------------------------------------

    module SuccessorSetMorphisms
      (N₁ : RawSuccessorSet a ℓ₁) (N₂ : RawSuccessorSet b ℓ₂)
      where

      open RawSuccessorSet N₁
        renaming (Carrier to A; _≈_ to _≈₁_; suc# to suc#₁; zero# to zero#₁)
      open RawSuccessorSet N₂
        renaming (Carrier to B; _≈_ to _≈₂_; suc# to suc#₂; zero# to zero#₂)
      open MorphismDefinitions A B _≈₂_

      record IsSuccessorSetHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
          suc#-homo         : Homomorphic₁ ⟦_⟧ suc#₁ suc#₂
          zero#-homo        : Homomorphic₀ ⟦_⟧ zero#₁ zero#₂

      record IsSuccessorSetMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isSuccessorSetHomomorphism : IsSuccessorSetHomomorphism ⟦_⟧
          injective                  : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsSuccessorSetHomomorphism isSuccessorSetHomomorphism public

        isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
        isRelMonomorphism = record
          { isHomomorphism = isRelHomomorphism
          ; injective      = injective
          }

      record IsSuccessorSetIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isSuccessorSetMonomorphism : IsSuccessorSetMonomorphism ⟦_⟧
          surjective                 : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsSuccessorSetMonomorphism isSuccessorSetMonomorphism public

        isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
        isRelIsomorphism = record
          { isMonomorphism = isRelMonomorphism
          ; surjective     = surjective
          }

    ------------------------------------------------------------------------
    -- Morphisms over magma-like structures
    ------------------------------------------------------------------------

    module MagmaMorphisms (M₁ : RawMagma a ℓ₁) (M₂ : RawMagma b ℓ₂) where

      open RawMagma M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_)
      open RawMagma M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_)
      open MorphismDefinitions A B _≈₂_

      record IsMagmaHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
          homo              : Homomorphic₂ ⟦_⟧ _∙_ _◦_

        open IsRelHomomorphism isRelHomomorphism public
          renaming (cong to ⟦⟧-cong)

      record IsMagmaMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
          injective           : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsMagmaHomomorphism isMagmaHomomorphism public

        isRelMonomorphism : IsRelMonomorphism _≈₁_ _≈₂_ ⟦_⟧
        isRelMonomorphism = record
          { isHomomorphism = isRelHomomorphism
          ; injective      = injective
          }

      record IsMagmaIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧
          surjective          : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsMagmaMonomorphism isMagmaMonomorphism public

        isRelIsomorphism : IsRelIsomorphism _≈₁_ _≈₂_ ⟦_⟧
        isRelIsomorphism = record
          { isMonomorphism = isRelMonomorphism
          ; surjective     = surjective
          }

    ------------------------------------------------------------------------
    -- Morphisms over monoid-like structures
    ------------------------------------------------------------------------

    module MonoidMorphisms (M₁ : RawMonoid a ℓ₁) (M₂ : RawMonoid b ℓ₂) where

      open RawMonoid M₁ renaming (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; ε to ε₁)
      open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; ε to ε₂)
      open MorphismDefinitions A B _≈₂_
      open MagmaMorphisms (RawMonoid.rawMagma M₁) (RawMonoid.rawMagma M₂)

      record IsMonoidHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isMagmaHomomorphism : IsMagmaHomomorphism ⟦_⟧
          ε-homo              : Homomorphic₀ ⟦_⟧ ε₁ ε₂

        open IsMagmaHomomorphism isMagmaHomomorphism public

      record IsMonoidMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
          injective            : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsMonoidHomomorphism isMonoidHomomorphism public

        isMagmaMonomorphism : IsMagmaMonomorphism ⟦_⟧
        isMagmaMonomorphism = record
          { isMagmaHomomorphism = isMagmaHomomorphism
          ; injective           = injective
          }

        open IsMagmaMonomorphism isMagmaMonomorphism public
          using (isRelMonomorphism)

      record IsMonoidIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
          surjective           : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsMonoidMonomorphism isMonoidMonomorphism public

        isMagmaIsomorphism : IsMagmaIsomorphism ⟦_⟧
        isMagmaIsomorphism = record
          { isMagmaMonomorphism = isMagmaMonomorphism
          ; surjective          = surjective
          }

        open IsMagmaIsomorphism isMagmaIsomorphism public
          using (isRelIsomorphism)

    ------------------------------------------------------------------------
    -- Morphisms over group-like structures
    ------------------------------------------------------------------------

    module GroupMorphisms (G₁ : RawGroup a ℓ₁) (G₂ : RawGroup b ℓ₂) where

      open RawGroup G₁ renaming
        (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁)
      open RawGroup G₂ renaming
        (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)
      open MorphismDefinitions A B _≈₂_
      open MagmaMorphisms  (RawGroup.rawMagma  G₁) (RawGroup.rawMagma  G₂)
      open MonoidMorphisms (RawGroup.rawMonoid G₁) (RawGroup.rawMonoid G₂)

      record IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isMonoidHomomorphism : IsMonoidHomomorphism ⟦_⟧
          ⁻¹-homo              : Homomorphic₁ ⟦_⟧ _⁻¹₁ _⁻¹₂

        open IsMonoidHomomorphism isMonoidHomomorphism public

      record IsGroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isGroupHomomorphism : IsGroupHomomorphism ⟦_⟧
          injective           : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsGroupHomomorphism isGroupHomomorphism public
          renaming (homo to ∙-homo)

        isMonoidMonomorphism : IsMonoidMonomorphism ⟦_⟧
        isMonoidMonomorphism = record
          { isMonoidHomomorphism = isMonoidHomomorphism
          ; injective            = injective
          }

        open IsMonoidMonomorphism isMonoidMonomorphism public
          using (isRelMonomorphism; isMagmaMonomorphism)

      record IsGroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isGroupMonomorphism : IsGroupMonomorphism ⟦_⟧
          surjective          : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsGroupMonomorphism isGroupMonomorphism public

        isMonoidIsomorphism : IsMonoidIsomorphism ⟦_⟧
        isMonoidIsomorphism = record
          { isMonoidMonomorphism = isMonoidMonomorphism
          ; surjective           = surjective
          }

        open IsMonoidIsomorphism isMonoidIsomorphism public
          using (isRelIsomorphism; isMagmaIsomorphism)

    ------------------------------------------------------------------------
    -- Morphisms over near-semiring-like structures
    ------------------------------------------------------------------------

    module NearSemiringMorphisms (R₁ : RawNearSemiring a ℓ₁) (R₂ : RawNearSemiring b ℓ₂) where

      open RawNearSemiring R₁ renaming
        ( Carrier to A; _≈_ to _≈₁_
        ; +-rawMonoid to +-rawMonoid₁
        ; _*_ to _*₁_
        ; *-rawMagma to *-rawMagma₁)

      open RawNearSemiring R₂ renaming
        ( Carrier to B; _≈_ to _≈₂_
        ; +-rawMonoid to +-rawMonoid₂
        ; _*_ to _*₂_
        ; *-rawMagma to *-rawMagma₂)

      private
        module + = MonoidMorphisms +-rawMonoid₁ +-rawMonoid₂
        module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂

      open MorphismDefinitions A B _≈₂_

      record IsNearSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          +-isMonoidHomomorphism : +.IsMonoidHomomorphism ⟦_⟧
          *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_

        open +.IsMonoidHomomorphism +-isMonoidHomomorphism public
          renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism)

        *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
        *-isMagmaHomomorphism = record
          { isRelHomomorphism = isRelHomomorphism
          ; homo = *-homo
          }

      record IsNearSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
          injective          : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsNearSemiringHomomorphism isNearSemiringHomomorphism public

        +-isMonoidMonomorphism : +.IsMonoidMonomorphism ⟦_⟧
        +-isMonoidMonomorphism = record
          { isMonoidHomomorphism = +-isMonoidHomomorphism
          ; injective            = injective
          }

        open +.IsMonoidMonomorphism +-isMonoidMonomorphism public
          using (isRelMonomorphism)
          renaming (isMagmaMonomorphism to +-isMagmaMonomorphsm)

        *-isMagmaMonomorphism : *.IsMagmaMonomorphism ⟦_⟧
        *-isMagmaMonomorphism = record
          { isMagmaHomomorphism = *-isMagmaHomomorphism
          ; injective           = injective
          }

      record IsNearSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isNearSemiringMonomorphism : IsNearSemiringMonomorphism ⟦_⟧
          surjective                 : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsNearSemiringMonomorphism isNearSemiringMonomorphism public

        +-isMonoidIsomorphism : +.IsMonoidIsomorphism ⟦_⟧
        +-isMonoidIsomorphism = record
          { isMonoidMonomorphism = +-isMonoidMonomorphism
          ; surjective           = surjective
          }

        open +.IsMonoidIsomorphism +-isMonoidIsomorphism public
          using (isRelIsomorphism)
          renaming (isMagmaIsomorphism to +-isMagmaIsomorphism)

        *-isMagmaIsomorphism : *.IsMagmaIsomorphism ⟦_⟧
        *-isMagmaIsomorphism = record
          { isMagmaMonomorphism = *-isMagmaMonomorphism
          ; surjective          = surjective
          }

    ------------------------------------------------------------------------
    -- Morphisms over semiring-like structures
    ------------------------------------------------------------------------

    module SemiringMorphisms (R₁ : RawSemiring a ℓ₁) (R₂ : RawSemiring b ℓ₂) where

      open RawSemiring R₁ renaming
        ( Carrier to A; _≈_ to _≈₁_
        ; 1# to 1#₁
        ; rawNearSemiring to rawNearSemiring₁
        ; *-rawMonoid to *-rawMonoid₁)

      open RawSemiring R₂ renaming
        ( Carrier to B; _≈_ to _≈₂_
        ; 1# to 1#₂
        ; rawNearSemiring to rawNearSemiring₂
        ; *-rawMonoid to *-rawMonoid₂)

      private
        module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂

      open MorphismDefinitions A B _≈₂_
      open NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂

      record IsSemiringHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isNearSemiringHomomorphism : IsNearSemiringHomomorphism ⟦_⟧
          1#-homo : Homomorphic₀ ⟦_⟧ 1#₁ 1#₂

        open IsNearSemiringHomomorphism isNearSemiringHomomorphism public

        *-isMonoidHomomorphism : *.IsMonoidHomomorphism ⟦_⟧
        *-isMonoidHomomorphism = record
          { isMagmaHomomorphism = *-isMagmaHomomorphism
          ; ε-homo = 1#-homo
          }

      record IsSemiringMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
          injective              : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsSemiringHomomorphism isSemiringHomomorphism public

        isNearSemiringMonomorphism : IsNearSemiringMonomorphism ⟦_⟧
        isNearSemiringMonomorphism = record
          { isNearSemiringHomomorphism = isNearSemiringHomomorphism
          ; injective = injective
          }

        open IsNearSemiringMonomorphism isNearSemiringMonomorphism public
          using (+-isMonoidMonomorphism; *-isMagmaMonomorphism)

        *-isMonoidMonomorphism : *.IsMonoidMonomorphism ⟦_⟧
        *-isMonoidMonomorphism = record
          { isMonoidHomomorphism = *-isMonoidHomomorphism
          ; injective            = injective
          }

      record IsSemiringIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isSemiringMonomorphism : IsSemiringMonomorphism ⟦_⟧
          surjective             : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsSemiringMonomorphism isSemiringMonomorphism public

        isNearSemiringIsomorphism : IsNearSemiringIsomorphism ⟦_⟧
        isNearSemiringIsomorphism = record
          { isNearSemiringMonomorphism = isNearSemiringMonomorphism
          ; surjective = surjective
          }

        open IsNearSemiringIsomorphism isNearSemiringIsomorphism public
          using (+-isMonoidIsomorphism; *-isMagmaIsomorphism)

        *-isMonoidIsomorphism : *.IsMonoidIsomorphism ⟦_⟧
        *-isMonoidIsomorphism = record
          { isMonoidMonomorphism = *-isMonoidMonomorphism
          ; surjective           = surjective
          }

    ------------------------------------------------------------------------
    -- Morphisms over ringWithoutOne-like structures
    ------------------------------------------------------------------------

    module RingWithoutOneMorphisms (R₁ : RawRingWithoutOne a ℓ₁) (R₂ : RawRingWithoutOne b ℓ₂) where

      open RawRingWithoutOne R₁ renaming
        ( Carrier to A; _≈_ to _≈₁_
        ; _*_ to _*₁_
        ; *-rawMagma to *-rawMagma₁
        ; +-rawGroup to +-rawGroup₁
        ; rawNearSemiring to rawNearSemiring₁)

      open RawRingWithoutOne R₂ renaming
        ( Carrier to B; _≈_ to _≈₂_
        ; _*_ to _*₂_
        ; *-rawMagma to *-rawMagma₂
        ; +-rawGroup to +-rawGroup₂
        ; rawNearSemiring to rawNearSemiring₂)

      private
        module + = GroupMorphisms  +-rawGroup₁  +-rawGroup₂
        module * = MagmaMorphisms *-rawMagma₁ *-rawMagma₂
        module +* = NearSemiringMorphisms rawNearSemiring₁ rawNearSemiring₂

      open MorphismDefinitions A B _≈₂_

      record IsRingWithoutOneHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          +-isGroupHomomorphism : +.IsGroupHomomorphism ⟦_⟧
          *-homo : Homomorphic₂ ⟦_⟧ _*₁_ _*₂_

        open +.IsGroupHomomorphism +-isGroupHomomorphism public
          renaming (homo to +-homo; ε-homo to 0#-homo; isMagmaHomomorphism to +-isMagmaHomomorphism; isMonoidHomomorphism to +-isMonoidHomomorphism)

        isNearSemiringHomomorphism : +*.IsNearSemiringHomomorphism ⟦_⟧
        isNearSemiringHomomorphism = record
          { +-isMonoidHomomorphism = +-isMonoidHomomorphism
          ; *-homo = *-homo
          }

        *-isMagmaHomomorphism : *.IsMagmaHomomorphism ⟦_⟧
        *-isMagmaHomomorphism = record
          { isRelHomomorphism = isRelHomomorphism
          ; homo = *-homo
          }

      record IsRingWithoutOneMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism ⟦_⟧
          injective                    : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public

        +-isGroupMonomorphism : +.IsGroupMonomorphism ⟦_⟧
        +-isGroupMonomorphism = record
          { isGroupHomomorphism = +-isGroupHomomorphism
          ; injective            = injective
          }

        open +.IsGroupMonomorphism +-isGroupMonomorphism public
          using (isRelMonomorphism)
          renaming (isMagmaMonomorphism to +-isMagmaMonomorphsm; isMonoidMonomorphism to +-isMonoidMonomorphism)

        *-isMagmaMonomorphism : *.IsMagmaMonomorphism ⟦_⟧
        *-isMagmaMonomorphism = record
          { isMagmaHomomorphism = *-isMagmaHomomorphism
          ; injective           = injective
          }

      record IsRingWithoutOneIsoMorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isRingWithoutOneMonomorphism : IsRingWithoutOneMonomorphism ⟦_⟧
          surjective                   : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsRingWithoutOneMonomorphism isRingWithoutOneMonomorphism public

        +-isGroupIsomorphism   : +.IsGroupIsomorphism ⟦_⟧
        +-isGroupIsomorphism  = record
          { isGroupMonomorphism = +-isGroupMonomorphism
          ; surjective           = surjective
          }

        open +.IsGroupIsomorphism +-isGroupIsomorphism public
          using (isRelIsomorphism)
          renaming (isMagmaIsomorphism to +-isMagmaIsomorphism; isMonoidIsomorphism to +-isMonoidIsomorphism)

        *-isMagmaIsomorphism : *.IsMagmaIsomorphism ⟦_⟧
        *-isMagmaIsomorphism = record
          { isMagmaMonomorphism = *-isMagmaMonomorphism
          ; surjective          = surjective
          }

    ------------------------------------------------------------------------
    -- Morphisms over ring-like structures
    ------------------------------------------------------------------------

    module RingMorphisms (R₁ : RawRing a ℓ₁) (R₂ : RawRing b ℓ₂) where

      open RawRing R₁ renaming
        ( Carrier to A; _≈_ to _≈₁_
        ; -_ to -₁_
        ; rawRingWithoutOne to rawRingWithoutOne₁
        ; rawSemiring to rawSemiring₁
        ; *-rawMonoid to *-rawMonoid₁
        ; +-rawGroup to +-rawGroup₁)

      open RawRing R₂ renaming
        ( Carrier to B; _≈_ to _≈₂_
        ; -_ to -₂_
        ; rawRingWithoutOne to rawRingWithoutOne₂
        ; rawSemiring to rawSemiring₂
        ; *-rawMonoid to *-rawMonoid₂
        ; +-rawGroup to +-rawGroup₂)

      module + = GroupMorphisms  +-rawGroup₁  +-rawGroup₂
      module * = MonoidMorphisms *-rawMonoid₁ *-rawMonoid₂
      module *+0 = RingWithoutOneMorphisms rawRingWithoutOne₁ rawRingWithoutOne₂

      open MorphismDefinitions A B _≈₂_
      open SemiringMorphisms rawSemiring₁ rawSemiring₂

      record IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
          -‿homo : Homomorphic₁ ⟦_⟧ -₁_ -₂_

        open IsSemiringHomomorphism isSemiringHomomorphism public

        +-isGroupHomomorphism : +.IsGroupHomomorphism ⟦_⟧
        +-isGroupHomomorphism = record
          { isMonoidHomomorphism = +-isMonoidHomomorphism
          ; ⁻¹-homo = -‿homo
          }

        isRingWithoutOneHomomorphism : *+0.IsRingWithoutOneHomomorphism ⟦_⟧
        isRingWithoutOneHomomorphism = record
          { +-isGroupHomomorphism = +-isGroupHomomorphism
          ; *-homo = *-homo
          }

      record IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isRingHomomorphism : IsRingHomomorphism ⟦_⟧
          injective          : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsRingHomomorphism isRingHomomorphism public

        isSemiringMonomorphism : IsSemiringMonomorphism ⟦_⟧
        isSemiringMonomorphism = record
          { isSemiringHomomorphism = isSemiringHomomorphism
          ; injective = injective
          }

        +-isGroupMonomorphism : +.IsGroupMonomorphism ⟦_⟧
        +-isGroupMonomorphism = record
          { isGroupHomomorphism = +-isGroupHomomorphism
          ; injective           = injective
          }

        open +.IsGroupMonomorphism +-isGroupMonomorphism
          using (isRelMonomorphism)
          renaming ( isMagmaMonomorphism to +-isMagmaMonomorphism
                   ; isMonoidMonomorphism to +-isMonoidMonomorphism
                   )

        *-isMonoidMonomorphism : *.IsMonoidMonomorphism ⟦_⟧
        *-isMonoidMonomorphism = record
          { isMonoidHomomorphism = *-isMonoidHomomorphism
          ; injective            = injective
          }

        open *.IsMonoidMonomorphism *-isMonoidMonomorphism public
          using ()
          renaming (isMagmaMonomorphism to *-isMagmaMonomorphism)

      record IsRingIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isRingMonomorphism : IsRingMonomorphism ⟦_⟧
          surjective         : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsRingMonomorphism isRingMonomorphism public

        isSemiringIsomorphism : IsSemiringIsomorphism ⟦_⟧
        isSemiringIsomorphism = record
          { isSemiringMonomorphism = isSemiringMonomorphism
          ; surjective = surjective
          }

        +-isGroupIsomorphism : +.IsGroupIsomorphism ⟦_⟧
        +-isGroupIsomorphism = record
          { isGroupMonomorphism = +-isGroupMonomorphism
          ; surjective          = surjective
          }

        open +.IsGroupIsomorphism +-isGroupIsomorphism
          using (isRelIsomorphism)
          renaming ( isMagmaIsomorphism to +-isMagmaIsomorphism
                   ; isMonoidIsomorphism to +-isMonoidIsomorphisn
                   )

        *-isMonoidIsomorphism : *.IsMonoidIsomorphism ⟦_⟧
        *-isMonoidIsomorphism = record
          { isMonoidMonomorphism = *-isMonoidMonomorphism
          ; surjective           = surjective
          }

        open *.IsMonoidIsomorphism *-isMonoidIsomorphism public
          using ()
          renaming (isMagmaIsomorphism to *-isMagmaIsomorphisn)

    ------------------------------------------------------------------------
    -- Morphisms over quasigroup-like structures
    ------------------------------------------------------------------------

    module QuasigroupMorphisms (Q₁ : RawQuasigroup a ℓ₁) (Q₂ : RawQuasigroup b ℓ₂) where

      open RawQuasigroup Q₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁;
                                      \\-rawMagma to \\-rawMagma₁; //-rawMagma to //-rawMagma₁;
                                      _≈_ to _≈₁_; _∙_ to _∙₁_; _\\_ to _\\₁_; _//_ to _//₁_)
      open RawQuasigroup Q₂ renaming (Carrier to B; ∙-rawMagma to ∙-rawMagma₂;
                                      \\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂;
                                      _≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_)

      module ∙  = MagmaMorphisms ∙-rawMagma₁ ∙-rawMagma₂
      module \\ = MagmaMorphisms \\-rawMagma₁ \\-rawMagma₂
      module // = MagmaMorphisms //-rawMagma₁ //-rawMagma₂

      open MorphismDefinitions A B _≈₂_

      record IsQuasigroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isRelHomomorphism : IsRelHomomorphism _≈₁_ _≈₂_ ⟦_⟧
          ∙-homo            : Homomorphic₂ ⟦_⟧ _∙₁_ _∙₂_
          \\-homo           : Homomorphic₂ ⟦_⟧ _\\₁_ _\\₂_
          //-homo           : Homomorphic₂ ⟦_⟧ _//₁_ _//₂_

        open IsRelHomomorphism isRelHomomorphism public
          renaming (cong to ⟦⟧-cong)

        ∙-isMagmaHomomorphism : ∙.IsMagmaHomomorphism ⟦_⟧
        ∙-isMagmaHomomorphism = record
          { isRelHomomorphism = isRelHomomorphism
          ; homo = ∙-homo
          }

        \\-isMagmaHomomorphism : \\.IsMagmaHomomorphism ⟦_⟧
        \\-isMagmaHomomorphism = record
          { isRelHomomorphism  = isRelHomomorphism
          ; homo = \\-homo
          }

        //-isMagmaHomomorphism : //.IsMagmaHomomorphism ⟦_⟧
        //-isMagmaHomomorphism = record
          { isRelHomomorphism  = isRelHomomorphism
          ; homo = //-homo
          }

      record IsQuasigroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧
          injective                : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsQuasigroupHomomorphism isQuasigroupHomomorphism public

        ∙-isMagmaMonomorphism   : ∙.IsMagmaMonomorphism ⟦_⟧
        ∙-isMagmaMonomorphism   = record
          { isMagmaHomomorphism = ∙-isMagmaHomomorphism
          ; injective           = injective
          }

        \\-isMagmaMonomorphism  : \\.IsMagmaMonomorphism ⟦_⟧
        \\-isMagmaMonomorphism  = record
          { isMagmaHomomorphism = \\-isMagmaHomomorphism
          ; injective           = injective
          }

        //-isMagmaMonomorphism  : //.IsMagmaMonomorphism ⟦_⟧
        //-isMagmaMonomorphism  = record
          { isMagmaHomomorphism = //-isMagmaHomomorphism
          ; injective           = injective
          }

        open //.IsMagmaMonomorphism //-isMagmaMonomorphism public
          using (isRelMonomorphism)

      record IsQuasigroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isQuasigroupMonomorphism : IsQuasigroupMonomorphism ⟦_⟧
          surjective               : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsQuasigroupMonomorphism isQuasigroupMonomorphism public

        ∙-isMagmaIsomorphism    : ∙.IsMagmaIsomorphism ⟦_⟧
        ∙-isMagmaIsomorphism    = record
          { isMagmaMonomorphism = ∙-isMagmaMonomorphism
          ; surjective          = surjective
          }

        \\-isMagmaIsomorphism   : \\.IsMagmaIsomorphism ⟦_⟧
        \\-isMagmaIsomorphism   = record
          { isMagmaMonomorphism = \\-isMagmaMonomorphism
          ; surjective          = surjective
          }

        //-isMagmaIsomorphism   : //.IsMagmaIsomorphism ⟦_⟧
        //-isMagmaIsomorphism   = record
          { isMagmaMonomorphism = //-isMagmaMonomorphism
          ; surjective          = surjective
          }

        open //.IsMagmaIsomorphism //-isMagmaIsomorphism public
          using (isRelIsomorphism)

    ------------------------------------------------------------------------
    -- Morphisms over loop-like structures
    ------------------------------------------------------------------------

    module LoopMorphisms (L₁ : RawLoop a ℓ₁) (L₂ : RawLoop b ℓ₂) where

      open RawLoop L₁ renaming (Carrier to A; ∙-rawMagma to ∙-rawMagma₁;
                                \\-rawMagma to \\-rawMagma₁; //-rawMagma to //-rawMagma₁;
                                 _≈_ to _≈₁_; _∙_ to _∙₁_; _\\_ to _\\₁_; _//_ to _//₁_; ε to ε₁)
      open RawLoop L₂ renaming (Carrier to B; ∙-rawMagma to ∙-rawMagma₂;
                                \\-rawMagma to \\-rawMagma₂; //-rawMagma to //-rawMagma₂;
                                _≈_ to _≈₂_; _∙_ to _∙₂_; _\\_ to _\\₂_; _//_ to _//₂_ ; ε to ε₂)
      open MorphismDefinitions A B _≈₂_

      open QuasigroupMorphisms (RawLoop.rawQuasigroup L₁) (RawLoop.rawQuasigroup L₂)

      record IsLoopHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isQuasigroupHomomorphism : IsQuasigroupHomomorphism ⟦_⟧
          ε-homo                   : Homomorphic₀ ⟦_⟧ ε₁ ε₂

        open IsQuasigroupHomomorphism isQuasigroupHomomorphism public

      record IsLoopMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isLoopHomomorphism   : IsLoopHomomorphism ⟦_⟧
          injective            : Injective _≈₁_ _≈₂_ ⟦_⟧

        open IsLoopHomomorphism isLoopHomomorphism public

      record IsLoopIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isLoopMonomorphism   : IsLoopMonomorphism ⟦_⟧
          surjective           : Surjective _≈₁_ _≈₂_ ⟦_⟧

        open IsLoopMonomorphism isLoopMonomorphism public

    ------------------------------------------------------------------------
    -- Morphisms over Kleene algebra structures
    ------------------------------------------------------------------------
    module KleeneAlgebraMorphisms (R₁ : RawKleeneAlgebra a ℓ₁) (R₂ : RawKleeneAlgebra b ℓ₂) where

      open RawKleeneAlgebra R₁ renaming
        ( Carrier to A; _≈_ to _≈₁_
        ; _⋆ to _⋆₁
        ; rawSemiring to rawSemiring₁
        )

      open RawKleeneAlgebra R₂ renaming
        ( Carrier to B; _≈_ to _≈₂_
        ; _⋆ to _⋆₂
        ; rawSemiring to rawSemiring₂
        )

      open MorphismDefinitions A B _≈₂_
      open SemiringMorphisms rawSemiring₁ rawSemiring₂

      record IsKleeneAlgebraHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
          ⋆-homo :  Homomorphic₁ ⟦_⟧ _⋆₁ _⋆₂

        open IsSemiringHomomorphism isSemiringHomomorphism public

      record IsKleeneAlgebraMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isKleeneAlgebraHomomorphism   : IsKleeneAlgebraHomomorphism ⟦_⟧
          injective                     : Injective  _≈₁_ _≈₂_ ⟦_⟧

        open IsKleeneAlgebraHomomorphism isKleeneAlgebraHomomorphism public

      record IsKleeneAlgebraIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂) where
        field
          isKleeneAlgebraMonomorphism   : IsKleeneAlgebraMonomorphism ⟦_⟧
          surjective                    : Surjective  _≈₁_ _≈₂_ ⟦_⟧

        open IsKleeneAlgebraMonomorphism isKleeneAlgebraMonomorphism public

    ------------------------------------------------------------------------
    -- Re-export contents of modules publicly

    open MagmaMorphisms public
    open MonoidMorphisms public
    open GroupMorphisms public
    open NearSemiringMorphisms public
    open SemiringMorphisms public
    open RingWithoutOneMorphisms public
    open RingMorphisms public
    open QuasigroupMorphisms public
    open LoopMorphisms public
    open KleeneAlgebraMorphisms public