------------------------------------------------------------------------
-- The Agda standard library
--
-- Basic definitions for morphisms between algebraic structures
------------------------------------------------------------------------

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

open import Relation.Binary.Core

module Algebra.Morphism.Definitions
  {a} (A : Set a)     -- The domain of the morphism
  {b} (B : Set b)     -- The codomain of the morphism
  {ℓ} (_≈_ : Rel B ℓ)  -- The equality relation over the codomain
  where

open import Algebra.Core
  using (Op₁; Op₂)

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

Homomorphic₀ : (A → B) → A → B → Set _
Homomorphic₀ ⟦_⟧ ∙ ∘ = $\begin{pmatrix} \,\href{Algebra.Morphism.Definitions.html#736}{\htmlId{744}{\htmlClass{Bound}{\text{∙}}}}\, \end{pmatrix}$ ≈ ∘

Homomorphic₁ : (A → B) → Op₁ A → Op₁ B → Set _
Homomorphic₁ ⟦_⟧ ∙_ ∘_ = ∀ x → $\begin{pmatrix} \,\href{Algebra.Morphism.Definitions.html#817}{\htmlId{833}{\htmlClass{Bound Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.Definitions.html#827}{\htmlId{835}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ≈ (∘ $\begin{pmatrix} \,\href{Algebra.Morphism.Definitions.html#827}{\htmlId{846}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$)

Homomorphic₂ : (A → B) → Op₂ A → Op₂ B → Set _
Homomorphic₂ ⟦_⟧ _∙_ _∘_ = ∀ x y → $\begin{pmatrix} \,\href{Algebra.Morphism.Definitions.html#928}{\htmlId{936}{\htmlClass{Bound}{\text{x}}}}\, \,\href{Algebra.Morphism.Definitions.html#916}{\htmlId{938}{\htmlClass{Bound Operator}{\text{∙}}}}\, \,\href{Algebra.Morphism.Definitions.html#930}{\htmlId{940}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$ ≈ ($\begin{pmatrix} \,\href{Algebra.Morphism.Definitions.html#928}{\htmlId{949}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ ∘ $\begin{pmatrix} \,\href{Algebra.Morphism.Definitions.html#930}{\htmlId{957}{\htmlClass{Bound}{\text{y}}}}\, \end{pmatrix}$)

------------------------------------------------------------------------
-- DEPRECATED NAMES
------------------------------------------------------------------------
-- Please use the new names as continuing support for the old names is
-- not guaranteed.

-- Version 1.3

Morphism : Set _
Morphism = A → B

{-# WARNING_ON_USAGE Morphism
"Warning: Morphism was deprecated in v1.3.
Please use the standard function notation (e.g. A → B) instead."
#-}