Agda UALib β

### Equation preservation

This section presents the Varieties.Preservation module of the Agda Universal Algebra Library. In this module we show that identities are preserved by closure operators H, S, and P. This will establish the easy direction of Birkhoffβs HSP Theorem.

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

open import Algebras.Signatures using (Signature; π; π₯)
open import Universes  using (Universe; _Μ)

module Varieties.Preservation {π : Signature π π₯} {π€ π§ : Universe}{X : π§ Μ} where

open import Varieties.Varieties {π = π}{π§}{X} public

π πβΊ πΎπ : Universe
π = ov π€
πβΊ = (ov π€) βΊ    -- (this will be the level of the relatively free algebra)
πΎπ = π€ β π§

```

#### H preserves identities

First we prove that the closure operator H is compatible with identities that hold in the given class.

```
module _ {fe : DFunExt} {π¦ : Pred (Algebra π€ π)(ov π€)} where

H-id1 : (p q : Term X) β π¦ β§ p β q β H{π€}{π€} π¦ β§ p β q
H-id1 p q Ξ± (hbase x) = β§-Lift-invar fe p q (Ξ± x)
H-id1 p q Ξ± (hlift{π¨} x) = β§-Lift-invar fe p q (H-id1 p q Ξ± x)

H-id1 p q Ξ± (hhimg{π¨}{πͺ} HA((π© , Ο , (Οhom , Οsur)), BβC)) = β§-I-invar fe πͺ p q Ξ³ BβC
where
Ξ² : π¨ β§ p β q
Ξ² = (H-id1 p q Ξ±) HA

preim : β π x β β£ π¨ β£
preim π x = Inv Ο (Οsur (π x))

ΞΆ : β π β Ο β (preim π) β‘ π
ΞΆ π = (fe π§ π€) Ξ» x β InvIsInv Ο (Οsur (π x))

Ξ³ = (fe πΎπ π€) Ξ» π β (π© β¦ p β§) π             β‘β¨ (ap (π© β¦ p β§) (ΞΆ π))β»ΒΉ β©
Ο((π¨ β¦ p β§)(preim π))   β‘β¨ ap Ο (happly Ξ² (preim π)) β©
Ο((π¨ β¦ q β§)(preim π))   β‘β¨ comm-hom-term (fe π₯ π€) π© (Ο , Οhom) q (preim π) β©
(π© β¦ q β§) π             β

H-id1 p q Ξ± (hiso{π¨}{π©} x xβ) = β§-I-invar fe π© p q (H-id1 p q Ξ± x) xβ

```

The converse of the foregoing result is almost too obvious to bother with. Nonetheless, we formalize it for completeness.

```
H-id2 : β {π¦} β (p q : Term X) β H{π€}{π¦} π¦ β§ p β q β π¦ β§ p β q

H-id2 p q Hpq KA = β§-lower-invar fe p q (Hpq (hbase KA))

```

#### S preserves identities

```
S-id1 : (p q : Term X) β π¦ β§ p β q β S{π€}{π€} π¦ β§ p β q

S-id1 p q Ξ± (sbase x) = β§-Lift-invar fe p q (Ξ± x)
S-id1 p q Ξ± (slift x) = β§-Lift-invar fe p q ((S-id1 p q Ξ±) x)

S-id1 p q Ξ± (ssub{π¨}{π©} sA Bβ€A) =
β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β-refl)
where --Apply S-β§ to the class π¦ βͺ ο½ π¨ ο½
Ξ² : π¨ β§ p β q
Ξ² = S-id1 p q Ξ± sA

Apq : ο½ π¨ ο½ β§ p β q
Apq refl = Ξ²

Ξ³ : (π¦ βͺ ο½ π¨ ο½) β§ p β q
Ξ³ {π©} (injβ x) = Ξ± x
Ξ³ {π©} (injβ y) = Apq y

S-id1 p q Ξ± (ssubw{π¨}{π©} sA Bβ€A) =
β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β-refl)
where  --Apply S-β§ to the class π¦ βͺ ο½ π¨ ο½
Ξ² : π¨ β§ p β q
Ξ² = S-id1 p q Ξ± sA

Apq : ο½ π¨ ο½ β§ p β q
Apq refl = Ξ²

Ξ³ : (π¦ βͺ ο½ π¨ ο½) β§ p β q
Ξ³ {π©} (injβ x) = Ξ± x
Ξ³ {π©} (injβ y) = Apq y

S-id1 p q Ξ± (siso{π¨}{π©} x xβ) = β§-I-invar fe π© p q (S-id1 p q Ξ± x) xβ

```

Again, the obvious converse is barely worth the bits needed to formalize it.

```
S-id2 : β{π¦}(p q : Term X) β S{π€}{π¦}π¦ β§ p β q β π¦ β§ p β q

S-id2 p q Spq {π¨} KA = β§-lower-invar fe p q (Spq (sbase KA))

```

#### P preserves identities

```
P-id1 : (p q : Term X) β π¦ β§ p β q β P{π€}{π€} π¦ β§ p β q

P-id1 p q Ξ± (pbase x) = β§-Lift-invar fe p q (Ξ± x)
P-id1 p q Ξ± (pliftu x) = β§-Lift-invar fe p q ((P-id1 p q Ξ±) x)
P-id1 p q Ξ± (pliftw x) = β§-Lift-invar fe p q ((P-id1 p q Ξ±) x)

P-id1 p q Ξ± (produ{I}{π} x) = β§-P-lift-invar I π  fe {p}{q} IH
where
IH : β i β (Lift-alg (π i) π€) β¦ p β§ β‘ (Lift-alg (π i) π€) β¦ q β§
IH i = β§-Lift-invar fe p q ((P-id1 p q Ξ±) (x i))

P-id1 p q Ξ± (prodw{I}{π} x) = β§-P-lift-invar I π fe {p}{q}IH
where
IH : β i β Lift-alg (π i) π€ β¦ p β§ β‘ Lift-alg (π i) π€ β¦ q β§
IH i = β§-Lift-invar fe p q ((P-id1 p q Ξ±) (x i))

P-id1 p q Ξ± (pisou{π¨}{π©} x xβ) = β§-I-invar fe π© p q (P-id1 p q Ξ± x) xβ
P-id1 p q Ξ± (pisow{π¨}{π©} x xβ) = β§-I-invar fe π© p q (P-id1 p q Ξ± x) xβ

```

β¦and converselyβ¦

```
P-id2 : β {π¦}(p q : Term X) β P{π€}{π¦} π¦ β§ p β q β π¦ β§ p β q
P-id2 p q PKpq KA = β§-lower-invar fe p q (PKpq (pbase KA))

```

#### V preserves identities

Finally, we prove the analogous preservation lemmas for the closure operator `V`.

```
V-id1 : (p q : Term X) β π¦ β§ p β q β V{π€}{π€} π¦ β§ p β q
V-id1 p q Ξ± (vbase x) = β§-Lift-invar fe p q (Ξ± x)
V-id1 p q Ξ± (vlift{π¨} x) = β§-Lift-invar  fe p q ((V-id1 p q Ξ±) x)
V-id1 p q Ξ± (vliftw{π¨} x) = β§-Lift-invar fe p q ((V-id1 p q Ξ±) x)

V-id1 p q Ξ± (vhimg{π¨}{πͺ}VA((π© , Ο , (Οh , ΟE)) , BβC)) = β§-I-invar fe πͺ p q Ξ³ BβC
where
IH : π¨ β§ p β q
IH = V-id1 p q Ξ± VA

preim : β π (x : X) β β£ π¨ β£
preim π x = (Inv Ο (ΟE (π x)))

ΞΆ : β π β Ο β (preim π) β‘ π
ΞΆ π = (fe π§ π€) Ξ» x β InvIsInv Ο (ΟE (π x))

Ξ³ = (fe πΎπ π€) Ξ» π β (π© β¦ p β§) π      β‘β¨ (ap (π© β¦ p β§) (ΞΆ π))β»ΒΉ β©
Ο ((π¨ β¦ p β§)(preim π))  β‘β¨ ap Ο (happly IH (preim π)) β©
Ο ((π¨ β¦ q β§)(preim π))  β‘β¨ comm-hom-term (fe π₯ π€) π© (Ο , Οh) q (preim π) β©
(π© β¦ q β§) π             β

V-id1 p q Ξ± (vssub {π¨}{π©} VA Bβ€A) = β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β-refl)
where
IH : π¨ β§ p β q
IH = V-id1 p q Ξ± VA

Asinglepq : ο½ π¨ ο½ β§ p β q
Asinglepq refl = IH

Ξ³ : (π¦ βͺ ο½ π¨ ο½) β§ p β q
Ξ³ {π©} (injβ x) = Ξ± x
Ξ³ {π©} (injβ y) = Asinglepq y

V-id1 p q Ξ± ( vssubw {π¨}{π©} VA Bβ€A ) =
β§-S-class-invar fe p q Ξ³ (π© , π¨ , (π© , Bβ€A) , injβ refl , β-refl)
where
IH : π¨ β§ p β q
IH = V-id1 p q Ξ± VA

Asinglepq : ο½ π¨ ο½ β§ p β q
Asinglepq refl = IH

Ξ³ : (π¦ βͺ ο½ π¨ ο½) β§ p β q
Ξ³ {π©} (injβ x) = Ξ± x
Ξ³ {π©} (injβ y) = Asinglepq y

V-id1 p q Ξ± (vprodu{I}{π} Vπ) = β§-P-invar I π fe {p}{q} Ξ» i β V-id1 p q Ξ± (Vπ i)
V-id1 p q Ξ± (vprodw{I}{π} Vπ) = β§-P-invar I π fe {p}{q} Ξ» i β V-id1 p q Ξ± (Vπ i)
V-id1 p q Ξ± (visou{π¨}{π©} VA AβB) = β§-I-invar fe π© p q (V-id1 p q Ξ± VA) AβB
V-id1 p q Ξ± (visow{π¨}{π©} VA AβB) = β§-I-invar fe π© p q (V-id1 p q Ξ± VA) AβB

-- module _ {π€ : Universe}{X : π€ Μ}{fe : DFunExt} {π¦ : Pred (Algebra π€ π)(ov π€)} where

-- open id1 {π€}{X}{(fe π€ π€) = fe π€ π€}{(fe π₯ π€) = fe π₯ π€}

V-id1' : (p q : Term X) β π¦ β§ p β q β V{π€}{ov π€ βΊ} π¦ β§ p β q

V-id1' p q Ξ± (vbase x) = β§-Lift-invar fe p q (Ξ± x)
V-id1' p q Ξ± (vlift{π¨} x) = β§-Lift-invar fe p q ((V-id1 p q Ξ±) x)
V-id1' p q Ξ± (vliftw{π¨} x) = β§-Lift-invar fe p q ((V-id1' p q Ξ±) x)

V-id1' p q Ξ± (vhimg{π¨}{πͺ} VA ((π© , Ο , (Οh , ΟE)) , BβC)) =
β§-I-invar fe πͺ p q Ξ³ BβC
where
IH : π¨ β§ p β q
IH = V-id1' p q Ξ± VA

preim : β π x β β£ π¨ β£
preim π x = (Inv Ο (ΟE (π x)))

ΞΆ : β π β Ο β (preim π) β‘ π
ΞΆ π = (fe π§ πβΊ) Ξ» x β InvIsInv Ο (ΟE (π x))

Ξ³ = (fe (π§ β πβΊ) πβΊ) Ξ» π β (π© β¦ p β§) π  β‘β¨ (ap (π© β¦ p β§) (ΞΆ π))β»ΒΉ  β©
(π© β¦ p β§) (Ο β (preim π)) β‘β¨(comm-hom-term (fe π₯ πβΊ) π© (Ο , Οh) p (preim π))β»ΒΉ β©
Ο((π¨ β¦ p β§)(preim π))     β‘β¨ ap Ο (happly IH (preim π))β©
Ο((π¨ β¦ q β§)(preim π))     β‘β¨ comm-hom-term (fe π₯ πβΊ) π© (Ο , Οh) q (preim π)β©
(π© β¦ q β§) π               β

V-id1' p q Ξ± (vssub{π¨}{π©} VA Bβ€A) = β§-S-invar fe π© {p}{q}(V-id1 p q Ξ± VA) Bβ€A
V-id1' p q Ξ± (vssubw {π¨}{π©} VA Bβ€A) = β§-S-invar fe π© {p}{q}(V-id1' p q Ξ± VA) Bβ€A
V-id1' p q Ξ± (vprodu{I}{π} Vπ) = β§-P-invar I π fe {p}{q} Ξ» i β V-id1 p q Ξ± (Vπ i)
V-id1' p q Ξ± (vprodw{I}{π} Vπ) = β§-P-invar I π fe {p}{q} Ξ» i β V-id1' p q Ξ± (Vπ i) -- {fwu = (fe πβΊ πβΊ)}{(fe π₯ πβΊ)}{(fe πβΊ πβΊ)}
V-id1' p q Ξ± (visou {π¨}{π©} VA AβB) = β§-I-invar fe π© p q (V-id1 p q Ξ± VA) AβB
V-id1' p q Ξ± (visow{π¨}{π©} VA AβB) = β§-I-invar fe π© p q (V-id1' p q Ξ± VA)AβB

```

#### Class identities

From `V-id1` it follows that if π¦ is a class of structures, then the set of identities modeled by all structures in `π¦` is equivalent to the set of identities modeled by all structures in `V π¦`. In other terms, `Th (V π¦)` is precisely the set of identities modeled by `π¦`. We formalize this observation as follows.

```
π± : Pred (Algebra (ov π€ βΊ) π) (ov π€ βΊ βΊ)
π± = V{π€}{ov π€ βΊ} π¦

class-ids-β : (p q : β£ π» X β£) β π¦ β§ p β q  β  (p , q) β Th π±
class-ids-β p q pKq VCloA = V-id1' p q pKq VCloA

class-ids-β : (p q : β£ π» X β£) β (p , q) β Th π± β  π¦ β§ p β q
class-ids-β p q Thpq {π¨} KA = β§-lower-invar fe p q (Thpq (vbase KA))

class-identities : (p q : β£ π» X β£) β π¦ β§ p β q  β  ((p , q) β Th π±)
class-identities p q = class-ids-β p q , class-ids-β p q

```

Once again, and for the last time, completeness dictates that we formalize the coverse of `V-id1`, however obvious it may be.

```
module _ {π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where

V-id2 : DFunExt β (p q : Term X) β (V{π€}{π¦} π¦ β§ p β q) β (π¦ β§ p β q)
V-id2 fe p q Vpq {π¨} KA = β§-lower-invar fe p q (Vpq (vbase KA))

```