------------------------------------------------------------------------ -- 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 ⟧