#### Homomorphic images of setoid algebras

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

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

open import Overture using (π ; π₯ ; Signature)

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

-- Imports from Agda and the Agda Standard Library ------------------------------------------
open import Agda.Primitive   using () renaming ( Set to Type )
open import Data.Product     using ( _,_ ; Ξ£-syntax )
renaming ( _Γ_ to _β§_ ; projβ to fst ; projβ to snd )
open import Function         using ( Func ; _on_ ; _β_ ; id )
open import Level            using ( Level ; _β_ ; suc )
open import Relation.Binary  using ( Setoid ; _Preserves_βΆ_ )
open import Relation.Unary   using ( Pred ; _β_ )

open import Relation.Binary.PropositionalEquality as β‘ using ()

-- Imports from the Agda Universal Algebra Library ---------------------------------------------
open import Overture          using  ( β£_β£ ; β₯_β₯ ; transport )
open  import Setoid.Functions
using ( liftβΌlower ; Ran ; _range ; _preimage ; _image ; Inv ; Image_β_ )
using ( _preimageβimage ; InvIsInverseΚ³ ; IsSurjective ; β-IsSurjective )

open  import Setoid.Algebras {π = π}
using ( Algebra ; ov ; _Μ_ ; β¨_β© ; Lift-AlgΛ‘ ; Lift-Alg ; π[_] )

open import Setoid.Homomorphisms.Basic {π = π}         using ( hom ; IsHom )
open import Setoid.Homomorphisms.Isomorphisms {π = π}  using ( _β_ ; Lift-β )

open  import Setoid.Homomorphisms.Properties {π = π}
using ( Lift-homΛ‘ ; ToLiftΛ‘ ; lift-hom-lemma ; πΎπΉ ; β-hom )

open Algebra

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

```

We begin with what seems, for our purposes, the most useful way to represent the class of homomorphic images of an algebra in dependent type theory.

```open IsHom

_IsHomImageOf_ : (π© : Algebra Ξ² Οα΅)(π¨ : Algebra Ξ± Οα΅) β Type _
π© IsHomImageOf π¨ = Ξ£[ Ο β hom π¨ π© ] IsSurjective β£ Ο β£

HomImages : Algebra Ξ± Οα΅ β Type (Ξ± β Οα΅ β ov (Ξ² β Οα΅))
HomImages {Ξ² = Ξ²}{Οα΅ = Οα΅} π¨ = Ξ£[ π© β Algebra Ξ² Οα΅ ] π© IsHomImageOf π¨

IdHomImage : {π¨ : Algebra Ξ± Οα΅} β π¨ IsHomImageOf π¨
IdHomImage {Ξ± = Ξ±}{π¨ = π¨} = πΎπΉ , Ξ» {y} β Image_β_.eq y refl
where open Setoid (Domain π¨) using ( refl )

```

These types should be self-explanatory, but just to be sure, letβs describe the Sigma type appearing in the second definition. Given an `π`-algebra `π¨ : Algebra Ξ± Ο`, the type `HomImages π¨` denotes the class `π¦` of algebras such that `π© β π¦` provided there is a surjective homomorphism from `π¨` to `π©`.

#### The image algebra of a hom

Here we show how to construct a Algebra (called `ImageAlgebra` below) that is the image of given hom.

```module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where
open Algebra π¨  renaming (Domain to A )                      using (Interp)
open Setoid A   renaming ( _β_ to _ββ_ ; Carrier to β£Aβ£)     using ()
open Algebra π©  renaming (Domain to B ; Interp to InterpB )  using ()
open Setoid B   renaming ( _β_ to _ββ_ ; refl to reflβ )     using ( reflexive )
renaming ( sym to symβ ; trans to transβ ; Carrier to β£Bβ£)
open Func       renaming (f to _β¨\$β©_ )                       using ( cong )
open IsHom

HomImageOf[_] : hom π¨ π© β Algebra (Ξ± β Ξ² β Οα΅) Οα΅
HomImageOf[ h ] =
record { Domain = Ran β£ h β£ ; Interp = record { f = f' ; cong = cong' } }
where
open Setoid(β¨ π β© (Ran β£ h β£))
using() renaming (Carrier to SRanh ; _β_ to _ββ_ ; refl to reflβ )

hhom :  β {π}(x : β₯ π β₯ π β β£ h β£ range )
β      (β£ h β£ β¨\$β© (π Μ π¨) ((β£ h β£ preimage) β x)) ββ (π Μ π©) ((β£ h β£ image) β x)

hhom {π} x = transβ (compatible β₯ h β₯) (cong InterpB (β‘.refl , (β£ h β£ preimageβimage) β x))

f' : SRanh β β£ h β£ range
f' (π , x) =  (π Μ π©)((β£ h β£ image)β x)        -- b : the image in β£Bβ£
, (π Μ π¨)((β£ h β£ preimage) β x)  -- a : the preimage in β£Aβ£
, hhom x                        -- p : proof that `(β£ h β£ β¨\$β© a) ββ b`

cong' : β {x y} β x ββ y β ((β£ h β£ image) (f' x)) ββ ((β£ h β£ image) (f' y))
cong' {(π , u)} {(.π , v)} (β‘.refl , EqA) = Goal
where
-- Alternative formulation of the goal:
goal : (π Μ π©)(Ξ» i β ((β£ h β£ image)(u i))) ββ (π Μ π©)(Ξ» i β ((β£ h β£ image) (v i)))
goal = cong InterpB (β‘.refl , EqA )

Goal : (β£ h β£ image) (f' (π , u)) ββ (β£ h β£ image) (f' (π , v))
Goal = goal
-- Note: `EqA : β i β (β£ h β£ image) (u i) ββ (β£ h β£ image) (v i)`
```

#### Homomorphic images of classes of setoid algebras

Given a class `π¦` of `π`-algebras, we need a type that expresses the assertion that a given algebra is a homomorphic image of some algebra in the class, as well as a type that represents all such homomorphic images.

```IsHomImageOfClass : {π¦ : Pred (Algebra Ξ± Οα΅)(suc Ξ±)} β Algebra Ξ± Οα΅ β Type (ov (Ξ± β Οα΅))
IsHomImageOfClass {π¦ = π¦} π© = Ξ£[ π¨ β Algebra _ _ ] ((π¨ β π¦) β§ (π© IsHomImageOf π¨))

HomImageOfClass : Pred (Algebra Ξ± Οα΅) (suc Ξ±) β Type (ov (Ξ± β Οα΅))
HomImageOfClass π¦ = Ξ£[ π© β Algebra _ _ ] IsHomImageOfClass {π¦ = π¦} π©
```

#### Lifting tools

Here are some tools that have been useful (e.g., in the road to the proof of Birkhoffβs HSP theorem). The first states and proves the simple fact that the lift of an epimorphism is an epimorphism.

```module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where
open Algebra π¨  using ()               renaming ( Domain to A )
open Algebra π©  using ()               renaming ( Domain to B )
open Setoid B   using ( sym ; trans )  renaming ( _β_ to _ββ_ )
open Func       using ( cong )         renaming ( f to _β¨\$β©_ )
open Level      using ( lift ; lower )

Lift-epi-is-epiΛ‘ :  (h : hom π¨ π©)(βα΅ βα΅ : Level)
β                  IsSurjective β£ h β£ β IsSurjective β£ Lift-homΛ‘ {π¨ = π¨}{π©} h βα΅ βα΅ β£

Lift-epi-is-epiΛ‘ h βα΅ βα΅ hepi {b} = Goal
where
open Algebra (Lift-AlgΛ‘ π© βα΅) using () renaming (Domain to lB )
open Setoid lB using () renaming ( _β_ to _βββ_ )

a : π[ π¨ ]
a = Inv β£ h β£ hepi

lem1 : b βββ (lift (lower b))
lem1 = liftβΌlower {π¨ = B} b

lem2' : (lower b) ββ (β£ h β£ β¨\$β© a)
lem2' = sym  (InvIsInverseΚ³ hepi)

lem2 : (lift (lower b)) βββ (lift (β£ h β£ β¨\$β© a))
lem2 = cong{From = B} β£ ToLiftΛ‘{π¨ = π©}{βα΅} β£ lem2'

lem3 : (lift (β£ h β£ β¨\$β© a)) βββ ((β£ Lift-homΛ‘ h βα΅ βα΅ β£ β¨\$β© lift a))
lem3 = lift-hom-lemma h a βα΅ βα΅

Ξ· : b βββ (β£ Lift-homΛ‘ h βα΅ βα΅ β£ β¨\$β© lift a)
Ξ· = trans lem1 (trans lem2 lem3)

Goal : Image β£ Lift-homΛ‘ h βα΅ βα΅ β£ β b
Goal = Image_β_.eq (lift a) Ξ·

Lift-Alg-hom-imageΛ‘ :  (βα΅ βα΅ : Level) β π© IsHomImageOf π¨
β                     (Lift-AlgΛ‘ π© βα΅) IsHomImageOf (Lift-AlgΛ‘ π¨ βα΅)

Lift-Alg-hom-imageΛ‘ βα΅ βα΅ ((Ο , Οhom) , Οepic) = Goal
where
lΟ : hom (Lift-AlgΛ‘ π¨ βα΅) (Lift-AlgΛ‘ π© βα΅)
lΟ = Lift-homΛ‘ {π¨ = π¨}{π©} (Ο , Οhom) βα΅ βα΅

lΟepic : IsSurjective β£ lΟ β£
lΟepic = Lift-epi-is-epiΛ‘ (Ο , Οhom) βα΅ βα΅ Οepic
Goal : (Lift-AlgΛ‘ π© βα΅) IsHomImageOf (Lift-AlgΛ‘ π¨ βα΅)
Goal = lΟ , lΟepic

module _ {π¨ : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where
open _β_
Lift-HomImage-lemma : β{Ξ³} β (Lift-Alg π¨ Ξ³ Ξ³) IsHomImageOf π© β π¨ IsHomImageOf π©
Lift-HomImage-lemma {Ξ³} Ο =  β-hom β£ Ο β£ (from Lift-β) ,
β-IsSurjective β₯ Ο β₯ (fromIsSurjective (Lift-β{π¨ = π¨}))

module _ {π¨ π¨' : Algebra Ξ± Οα΅}{π© : Algebra Ξ² Οα΅} where
open _β_
HomImage-β : π¨ IsHomImageOf π¨' β π¨ β π© β π© IsHomImageOf π¨'
HomImage-β Ο AβB = β-hom β£ Ο β£ (to AβB) , β-IsSurjective β₯ Ο β₯ (toIsSurjective AβB)

HomImage-β' : π¨ IsHomImageOf π¨' β π¨' β π© β π¨ IsHomImageOf π©
HomImage-β' Ο A'βB = (β-hom (from A'βB) β£ Ο β£) , β-IsSurjective (fromIsSurjective A'βB) β₯ Ο β₯
```