#### Homomorphisms of Algebras over Setoids

This is the Setoid.Homomorphisms.Basic module of the Agda Universal Algebra Library.

```{-# OPTIONS --without-K --exact-split --safe #-}

open import Base.Algebras.Basic using (π ; π₯ ; Signature )

module Setoid.Homomorphisms.Basic {π : Signature π π₯} where

-- Imports from Agda and the Agda Standard Library ------------------------------
open import Agda.Primitive    using ( _β_ ; Level )  renaming ( Set to Type )
open import Data.Product      using ( _,_ ; Ξ£ ; Ξ£-syntax )
open import Function.Bundles  using ()               renaming ( Func to _βΆ_ )
open import Relation.Binary   using ( Setoid )

-- Imports from the Agda Universal Algebra Library ---------------------------
open import Base.Overture.Preliminaries    using ( β£_β£ ; β₯_β₯ )
open import Setoid.Overture.Injective      using ( IsInjective )
open import Setoid.Overture.Surjective     using ( IsSurjective )
open import Setoid.Algebras.Basic {π = π}  using ( Algebra ; _Μ_ )

private variable
Ξ± Ξ² Οα΅ Οα΅ : Level

module _ (π¨ : Algebra Ξ± Οα΅)(π© : Algebra Ξ² Οα΅) where
open Algebra π¨  using () renaming (Domain to A )
open Algebra π©  using () renaming (Domain to B )
open Setoid A   using () renaming ( _β_ to _ββ_ )
open Setoid B   using () renaming ( _β_ to _ββ_ )
open _βΆ_ {a = Ξ±}{Οα΅}{Ξ²}{Οα΅}{From = A}{To = B} renaming (f to _β¨\$β©_ )

compatible-map-op : (A βΆ B) β β£ π β£ β Type (π₯ β Ξ± β Οα΅)
compatible-map-op h f = β {a} β (h β¨\$β© ((f Μ π¨) a)) ββ ((f Μ π©) (Ξ» x β (h β¨\$β© (a x))))

compatible-map : (A βΆ B) β Type (π β π₯ β Ξ± β Οα΅)
compatible-map h = β {f} β compatible-map-op h f

-- The property of being a homomorphism.
record IsHom (h : A βΆ B) : Type (π β π₯ β Ξ± β Οα΅ β Οα΅) where
field
compatible : compatible-map h

hom : Type (π β π₯ β Ξ± β Οα΅ β Ξ² β Οα΅)
hom = Ξ£ (A βΆ B) IsHom

```

#### Monomorphisms and epimorphisms

``` record IsMon (h : A βΆ B) : Type (π β π₯ β Ξ± β Οα΅ β Ξ² β Οα΅) where
field
isHom : IsHom h
isInjective : IsInjective h

HomReduct : hom
HomReduct = h , isHom

mon : Type (π β π₯ β Ξ± β Οα΅ β Ξ² β Οα΅)
mon = Ξ£ (A βΆ B) IsMon

monβhom : mon β hom
monβhom h = IsMon.HomReduct β₯ h β₯

record IsEpi (h : A βΆ B) : Type (π β π₯ β Ξ± β Οα΅ β Ξ² β Οα΅) where
field
isHom : IsHom h
isSurjective : IsSurjective h

HomReduct : hom
HomReduct = h , isHom

epi : Type (π β π₯ β Ξ± β Οα΅ β Ξ² β Οα΅)
epi = Ξ£ (A βΆ B) IsEpi

epiβhom : epi β hom
epiβhom h = IsEpi.HomReduct β₯ h β₯

module _ (π¨ : Algebra Ξ± Οα΅)(π© : Algebra Ξ² Οα΅) where
open IsEpi
open IsMon

monβintohom : mon π¨ π© β Ξ£[ h β hom π¨ π© ] IsInjective β£ h β£
monβintohom (hh , hhM) = (hh , isHom hhM) , isInjective hhM

epiβontohom : epi π¨ π© β Ξ£[ h β hom π¨ π© ] IsSurjective β£ h β£
epiβontohom (hh , hhE) = (hh , isHom hhE) , isSurjective hhE

```