### Homomorphic Images

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

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

open import Algebras.Basic

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

-- Imports from Agda and the Agda Standard Library ------------------------------------------
open import Agda.Primitive using ( _β_ ; lsuc ) renaming ( Set to Type )
open import Data.Product   using ( _,_ ; Ξ£-syntax ; Ξ£ ; _Γ_ )
open import Level          using ( Level )
open import Relation.Binary.PropositionalEquality
using ( _β‘_ ; module β‘-Reasoning ; cong ; cong-app ; sym )
open import Relation.Unary using ( Pred ; _β_ )

-- Imports from the Agda Universal Algebra Library ------------------------------------------
open import Overture.Preliminaries      using ( ππ ; β£_β£ ; β₯_β₯ ; lowerβΌlift ; liftβΌlower )
open import Overture.Inverses           using ( Image_β_ ; Inv ; InvIsInverseΚ³ ; eq )
open import Overture.Surjective         using ( IsSurjective )
open import Algebras.Products   {π = π} using ( ov )
open import Homomorphisms.Basic {π = π} using ( hom ; ππΎπ»π ; πβ΄πβ―π )
open import Homomorphisms.Properties {π = π} using ( Lift-hom )

```

#### Images of a single algebra

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.

```module _ {Ξ± Ξ² : Level } where

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

HomImages : Algebra Ξ± π β Type(π β π₯ β Ξ± β lsuc Ξ²)
HomImages π¨ = Ξ£[ π© β Algebra Ξ² π ] π© IsHomImageOf π¨

```

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 `π© : Algebra Ξ² π` with a map `Ο : β£ π¨ β£ β β£ π© β£` such that `Ο` is a surjective homomorphism.

#### Images of a class of 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.

```module _ {Ξ± : Level} where

IsHomImageOfClass : {π¦ : Pred (Algebra Ξ± π)(lsuc Ξ±)} β Algebra Ξ± π β Type(ov Ξ±)
IsHomImageOfClass {π¦ = π¦} π© = Ξ£[ π¨ β Algebra Ξ± π ] ((π¨ β π¦) Γ (π© IsHomImageOf π¨))

HomImageOfClass : Pred (Algebra Ξ± π) (lsuc Ξ±) β 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 _ {Ξ± Ξ² : Level} where

open Level
open β‘-Reasoning

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

Lift-epi-is-epi {π¨ = π¨} βα΅ {π©} βα΅ h hepi y = eq (lift a) Ξ·
where
lh : hom (Lift-Alg π¨ βα΅) (Lift-Alg π© βα΅)
lh = Lift-hom βα΅ {π©} βα΅ h

ΞΆ : Image β£ h β£ β (lower y)
ΞΆ = hepi (lower y)

a : β£ π¨ β£
a = Inv β£ h β£ ΞΆ

Ξ½ : lift (β£ h β£ a) β‘ β£ Lift-hom βα΅ {π©} βα΅ h β£ (Level.lift a)
Ξ½ = cong (Ξ» - β lift (β£ h β£ (- a))) (lowerβΌlift {Level-of-Carrier π¨}{Ξ²})

Ξ· : y β‘ β£ lh β£ (lift a)
Ξ· = y               β‘β¨ (cong-app liftβΌlower) y β©
lift (lower y)  β‘β¨ cong lift (sym (InvIsInverseΚ³ ΞΆ)) β©
lift (β£ h β£ a)  β‘β¨ Ξ½ β©
β£ lh β£ (lift a) β

Lift-Alg-hom-image : {π¨ : Algebra Ξ± π}(βα΅ : Level){π© : Algebra Ξ² π}(βα΅ : Level)