------------------------------------------------------------------------
-- 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 ⟧
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4