```------------------------------------------------------------------------
-- 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 : Set) (to : Setoid) where
open Setoid to renaming (carrier to to-carrier)

Morphism : Set
Morphism = from → to-carrier

Homomorphic₀ : Morphism → from → to-carrier → 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) (setoid 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
```