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

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

    open import Relation.Binary.Core

    module Relation.Binary.Morphism.Definitions
      {a} (A : Set a)     -- The domain of the morphism
      {b} (B : Set b)     -- The codomain of the morphism
      where

    open import Level using (Level)

    private
      variable
        ℓ₁ ℓ₂ : Level

    ------------------------------------------------------------------------
    -- Morphism definition in Function.Core

    open import Function.Core public
      using (Morphism)

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

    Homomorphic₂ : Rel A ℓ₁ → Rel B ℓ₂ → (A → B) → Set _
    Homomorphic₂ _∼₁_ _∼₂_ ⟦_⟧ = ∀ {x y} → x ∼₁ y → ⟦ x ⟧ ∼₂ ⟦ y ⟧