    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Bundled definitions of homomorphisms between algebras
    --
    -- NB indexed by Raw bundles, just as IsXHomomorphism is
    ------------------------------------------------------------------------

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

    module Algebra.Morphism.Bundles where

    open import Algebra.Bundles.Raw using
      ( RawMagma; RawMonoid; RawGroup; RawQuasigroup; RawLoop
      ; RawSemiring; RawNearSemiring; RawKleeneAlgebra
      ; RawRingWithoutOne; RawRing)
    open import Algebra.Morphism.Structures
    open import Level using (Level; suc; _⊔_)
    --open import Relation.Binary.Morphism using (IsRelHomomorphism)
    --open import Relation.Binary.Morphism.Bundles using (SetoidHomomorphism)

    private
      variable
        ℓ a ℓa b ℓb : Level

    ------------------------------------------------------------------------
    -- Morphisms between Magmas
    ------------------------------------------------------------------------

    record MagmaHomomorphism
      (A : RawMagma a ℓa) (B : RawMagma b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb)
      where
      private
        module A = RawMagma A
        module B = RawMagma B

      field
        ⟦_⟧ : A.Carrier → B.Carrier

        isMagmaHomomorphism : IsMagmaHomomorphism A B ⟦_⟧

      open IsMagmaHomomorphism isMagmaHomomorphism public

    ------------------------------------------------------------------------
    -- Morphisms between Monoids
    ------------------------------------------------------------------------

    record MonoidHomomorphism
      (A : RawMonoid a ℓa) (B : RawMonoid b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb)
      where
      private
        module A = RawMonoid A
        module B = RawMonoid B

      field
        ⟦_⟧ : A.Carrier → B.Carrier

        isMonoidHomomorphism : IsMonoidHomomorphism A B ⟦_⟧

      open IsMonoidHomomorphism isMonoidHomomorphism public

      magmaHomomorphism : MagmaHomomorphism A.rawMagma B.rawMagma
      magmaHomomorphism = record { isMagmaHomomorphism = isMagmaHomomorphism }

    ------------------------------------------------------------------------
    -- Morphisms between Groups
    ------------------------------------------------------------------------

    record GroupHomomorphism
      (A : RawGroup a ℓa) (B : RawGroup b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb)
      where
      private
        module A = RawGroup A
        module B = RawGroup B

      field
        ⟦_⟧ : A.Carrier → B.Carrier

        isGroupHomomorphism : IsGroupHomomorphism A B ⟦_⟧

      open IsGroupHomomorphism isGroupHomomorphism public

      monoidHomomorphism : MonoidHomomorphism A.rawMonoid B.rawMonoid
      monoidHomomorphism = record { isMonoidHomomorphism = isMonoidHomomorphism }

      open MonoidHomomorphism monoidHomomorphism public
        using (magmaHomomorphism)

    ------------------------------------------------------------------------
    -- Morphisms between NearSemirings
    ------------------------------------------------------------------------

    record NearSemiringHomomorphism
      (A : RawNearSemiring a ℓa) (B : RawNearSemiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb)
      where
      private
        module A = RawNearSemiring A
        module B = RawNearSemiring B

      field
        ⟦_⟧ : A.Carrier → B.Carrier

        isNearSemiringHomomorphism : IsNearSemiringHomomorphism A B ⟦_⟧

      open IsNearSemiringHomomorphism isNearSemiringHomomorphism public

      +-monoidHomomorphism : MonoidHomomorphism A.+-rawMonoid B.+-rawMonoid
      +-monoidHomomorphism = record { isMonoidHomomorphism = +-isMonoidHomomorphism }

      *-magmaHomomorphism : MagmaHomomorphism A.*-rawMagma B.*-rawMagma
      *-magmaHomomorphism = record { isMagmaHomomorphism = *-isMagmaHomomorphism }

      open MonoidHomomorphism +-monoidHomomorphism public
        using ()
        renaming (magmaHomomorphism to +-magmaHomomorphism)

    ------------------------------------------------------------------------
    -- Morphisms between Semirings
    ------------------------------------------------------------------------

    record SemiringHomomorphism
      (A : RawSemiring a ℓa) (B : RawSemiring b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb)
      where
      private
        module A = RawSemiring A
        module B = RawSemiring B

      field
        ⟦_⟧ : A.Carrier → B.Carrier

        isSemiringHomomorphism : IsSemiringHomomorphism A B ⟦_⟧

      open IsSemiringHomomorphism isSemiringHomomorphism public

      nearSemiringHomomorphism : NearSemiringHomomorphism A.rawNearSemiring B.rawNearSemiring
      nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism }

      open NearSemiringHomomorphism nearSemiringHomomorphism public
        using (*-magmaHomomorphism; +-monoidHomomorphism; +-magmaHomomorphism)

      *-monoidHomomorphism : MonoidHomomorphism A.*-rawMonoid B.*-rawMonoid
      *-monoidHomomorphism = record { isMonoidHomomorphism = *-isMonoidHomomorphism }

    ------------------------------------------------------------------------
    -- Morphisms between KleeneAlgebras
    ------------------------------------------------------------------------

    record KleeneAlgebraHomomorphism
      (A : RawKleeneAlgebra a ℓa) (B : RawKleeneAlgebra b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb)
      where
      private
        module A = RawKleeneAlgebra A
        module B = RawKleeneAlgebra B

      field
        ⟦_⟧ : A.Carrier → B.Carrier
        isKleeneAlgebraHomomorphism : IsKleeneAlgebraHomomorphism A B ⟦_⟧

      open IsKleeneAlgebraHomomorphism isKleeneAlgebraHomomorphism public

      semiringHomomorphism : SemiringHomomorphism A.rawSemiring B.rawSemiring
      semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism }

      open SemiringHomomorphism semiringHomomorphism public
        hiding (*-isMagmaHomomorphism; *-isMonoidHomomorphism)

    ------------------------------------------------------------------------
    -- Morphisms between RingWithoutOnes
    ------------------------------------------------------------------------

    record RingWithoutOneHomomorphism (A : RawRingWithoutOne a ℓa) (B : RawRingWithoutOne b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where
      private
        module A = RawRingWithoutOne A
        module B = RawRingWithoutOne B

      field
        ⟦_⟧ : A.Carrier → B.Carrier
        isRingWithoutOneHomomorphism : IsRingWithoutOneHomomorphism A B ⟦_⟧

      open IsRingWithoutOneHomomorphism isRingWithoutOneHomomorphism public

      nearSemiringHomomorphism : NearSemiringHomomorphism A.rawNearSemiring B.rawNearSemiring
      nearSemiringHomomorphism = record { isNearSemiringHomomorphism = isNearSemiringHomomorphism }

      open NearSemiringHomomorphism nearSemiringHomomorphism public
        using (*-magmaHomomorphism; +-magmaHomomorphism; +-monoidHomomorphism)

      +-groupHomomorphism : GroupHomomorphism A.+-rawGroup B.+-rawGroup
      +-groupHomomorphism = record { isGroupHomomorphism = +-isGroupHomomorphism }

    ------------------------------------------------------------------------
    -- Morphisms between Rings
    ------------------------------------------------------------------------

    record RingHomomorphism (A : RawRing a ℓa) (B : RawRing b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb) where
      private
        module A = RawRing A
        module B = RawRing B

      field
        ⟦_⟧ : A.Carrier → B.Carrier
        isRingHomomorphism : IsRingHomomorphism A B ⟦_⟧

      open IsRingHomomorphism isRingHomomorphism public

      ringWithoutOneHomomorphism : RingWithoutOneHomomorphism A.rawRingWithoutOne B.rawRingWithoutOne
      ringWithoutOneHomomorphism = record { isRingWithoutOneHomomorphism = isRingWithoutOneHomomorphism }

      open RingWithoutOneHomomorphism ringWithoutOneHomomorphism public
        using (+-groupHomomorphism)

      semiringHomomorphism : SemiringHomomorphism A.rawSemiring B.rawSemiring
      semiringHomomorphism = record { isSemiringHomomorphism = isSemiringHomomorphism }

      open SemiringHomomorphism semiringHomomorphism public
        using ( nearSemiringHomomorphism
              ; *-monoidHomomorphism; *-magmaHomomorphism
              ; +-monoidHomomorphism; +-magmaHomomorphism)

    ------------------------------------------------------------------------
    -- Morphisms between Quasigroups
    ------------------------------------------------------------------------

    record QuasigroupHomomorphism
      (A : RawQuasigroup a ℓa) (B : RawQuasigroup b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb)
      where
      private
        module A = RawQuasigroup A
        module B = RawQuasigroup B

      field
        ⟦_⟧ : A.Carrier → B.Carrier
        isQuasigroupHomomorphism : IsQuasigroupHomomorphism A B ⟦_⟧

      open IsQuasigroupHomomorphism isQuasigroupHomomorphism public

      magmaHomomorphism : MagmaHomomorphism A.∙-rawMagma B.∙-rawMagma
      magmaHomomorphism = record { isMagmaHomomorphism = ∙-isMagmaHomomorphism }

    ------------------------------------------------------------------------
    -- Morphisms between Loops
    ------------------------------------------------------------------------

    record LoopHomomorphism
      (A : RawLoop a ℓa) (B : RawLoop b ℓb) : Set (a ⊔ b ⊔ ℓa ⊔ ℓb)
      where
      private
        module A = RawLoop A
        module B = RawLoop B

      field
        ⟦_⟧ : A.Carrier → B.Carrier
        isLoopHomomorphism : IsLoopHomomorphism A B ⟦_⟧

      open IsLoopHomomorphism isLoopHomomorphism public

      quasigroupHomomorphism : QuasigroupHomomorphism A.rawQuasigroup B.rawQuasigroup
      quasigroupHomomorphism = record { isQuasigroupHomomorphism = isQuasigroupHomomorphism }