module Algebra.Morphism where
open import Relation.Binary
open import Algebra
open import Algebra.FunctionProperties
open import Data.Function
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 ⟧)
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