```------------------------------------------------------------------------
-- Morphisms between algebraic structures
------------------------------------------------------------------------

module Algebra.Morphism where

open import Relation.Binary
open import Algebra
open import Algebra.FunctionProperties
open import Data.Function

------------------------------------------------------------------------
-- Basic definitions

module Definitions (From To : Set) (_≈_ : Rel To) where
Morphism : Set
Morphism = From → To

Homomorphic₀ : Morphism → From → To → Set
Homomorphic₀ ⟦_⟧ ∙ ∘ = ⟦ ∙ ⟧ ≈ ∘

Homomorphic₁ : Morphism → Fun₁ From → Op₁ To → Set
Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → ⟦ ∙ x ⟧ ≈ ∘ ⟦ x ⟧

Homomorphic₂ : Morphism → Fun₂ From → Op₂ To → Set
Homomorphic₂ ⟦_⟧ _∙_ _∘_ =
∀ x y → ⟦ x ∙ y ⟧ ≈ (⟦ x ⟧ ∘ ⟦ y ⟧)

------------------------------------------------------------------------
-- Some specific morphisms

-- Other morphisms could of course be defined.

record _-RawRing⟶_ (From To : RawRing) : Set where
open RawRing
open Definitions (carrier From) (carrier To) (_≈_ To)
field
⟦_⟧    : Morphism
+-homo : Homomorphic₂ ⟦_⟧ (_+_ From) (_+_ To)
*-homo : Homomorphic₂ ⟦_⟧ (_*_ From) (_*_ To)
-‿homo : Homomorphic₁ ⟦_⟧ (-_  From) (-_  To)
0-homo : Homomorphic₀ ⟦_⟧ (0#  From) (0#  To)
1-homo : Homomorphic₀ ⟦_⟧ (1#  From) (1#  To)

_-Ring⟶_ : Ring → Ring → Set
From -Ring⟶ To = rawRing From -RawRing⟶ rawRing To
where open Ring
```