### Properties of Homomorphisms

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

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

open import Algebras.Basic

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

-- Imports from Agda and the Agda Standard Library --------------------------------
open import Data.Product   using ( _,_ )
open import Function.Base  using ( _β_ )
open import Level          using ( Level )
open import Relation.Binary.PropositionalEquality
using ( _β‘_ ; module β‘-Reasoning ; cong ; refl )

-- -- Imports from the Agda Universal Algebras Library --------------------------------
open import Overture.Preliminaries       using ( β£_β£ ; β₯_β₯ )
open import Homomorphisms.Basic  {π = π} using ( hom ; is-homomorphism )
private variable Ξ± Ξ² Ξ³ Ο : Level

```

#### Homomorphism composition

The composition of homomorphisms is again a homomorphism. We formalize this in a number of alternative ways.

```open β‘-Reasoning

module _ (π¨ : Algebra Ξ± π){π© : Algebra Ξ² π}(πͺ : Algebra Ξ³ π) where

β-hom : hom π¨ π©  β  hom π© πͺ  β  hom π¨ πͺ
β-hom (g , ghom) (h , hhom) = h β g , Goal where

Goal : β π a β (h β g)((π Μ π¨) a) β‘ (π Μ πͺ)(h β g β a)
Goal π a = (h β g)((π Μ π¨) a)     β‘β¨ cong h ( ghom π a ) β©
h ((π Μ π©)(g β a))     β‘β¨ hhom π ( g β a ) β©
(π Μ πͺ)(h β g β a)     β

β-is-hom : {f : β£ π¨ β£ β β£ π© β£}{g : β£ π© β£ β β£ πͺ β£}
β         is-homomorphism π¨ π© f β is-homomorphism π© πͺ g β is-homomorphism π¨ πͺ (g β f)
β-is-hom {f} {g} fhom ghom = β₯ β-hom (f , fhom) (g , ghom) β₯

```

A homomorphism from `π¨` to `π©` can be lifted to a homomorphism from `Lift-Alg π¨ βα΅` to `Lift-Alg π© βα΅`.

```open Level

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

Lift-hom {π¨ = π¨} βα΅ {π©} βα΅ (f , fhom) = lift β f β lower , Goal
where
lABh : is-homomorphism (Lift-Alg π¨ βα΅) π© (f β lower)
lABh = β-is-hom (Lift-Alg π¨ βα΅) π© {lower}{f} (Ξ» _ _ β refl) fhom

Goal : is-homomorphism(Lift-Alg π¨ βα΅)(Lift-Alg π© βα΅) (lift β (f β lower))
Goal = β-is-hom (Lift-Alg π¨ βα΅) (Lift-Alg π© βα΅){f β lower}{lift} lABh Ξ» _ _ β refl

```

We should probably point out that while the lifting and lowering homomorphisms are important for our formal treatment of algebras in type theory, they never ariseβin fact, they are not even definableβin classical universal algebra based on set theory.