### Closure Operators

Fix a signature `π`, let `π¦` be a class of `π`-algebras, and define

• `H π¦` = algebras isomorphic to a homomorphic image of a member of `π¦`;
• `S π¦` = algebras isomorphic to a subalgebra of a member of `π¦`;
• `P π¦` = algebras isomorphic to a product of members of `π¦`.

A straight-forward verification confirms that `H`, `S`, and `P` are closure operators (expansive, monotone, and idempotent). A class `π¦` of `π`-algebras is said to be closed under the taking of homomorphic images provided `H π¦ β π¦`. Similarly, `π¦` is closed under the taking of subalgebras (resp., arbitrary products) provided `S π¦ β π¦` (resp., `P π¦ β π¦`). The operators `H`, `S`, and `P` can be composed with one another repeatedly, forming yet more closure operators.

An algebra is a homomorphic image (resp., subalgebra; resp., product) of every algebra to which it is isomorphic. Thus, the class `H π¦` (resp., `S π¦`; resp., `P π¦`) is closed under isomorphism.

A variety is a class of algebras, in the same signature, that is closed under the taking of homomorphic images, subalgebras, and arbitrary products. To represent varieties we define inductive types for the closure operators `H`, `S`, and `P` that are composable. Separately, we define an inductive type `V` which simultaneously represents closure under all three operators, `H`, `S`, and `P`.

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

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

module Base.Varieties.Closure {π : Signature π π₯} where

-- Imports from Agda and the Agda Standard Library ---------------------------------------
open import Agda.Primitive  using () renaming ( Set to Type )
open import Level           using ( Level ;  Lift ; _β_ ; suc )
open import Relation.Unary  using ( Pred ; _β_ ; _β_ )
open import Data.Product    using ( _,_ ; Ξ£-syntax )
renaming ( projβ to fst ; projβ to snd )

open  import Axiom.Extensionality.Propositional
using () renaming ( Extensionality to funext )

-- Imports from the Agda Universal Algebra Library ---------------------------------------
open import Overture               using ( β£_β£ ; β₯_β₯ )
open import Base.Algebras {π = π}  using ( Algebra ; Lift-Alg ; ov ; β¨ )

open  import Base.Homomorphisms {π = π}
using ( _β_ ; β-sym ; Lift-β ; β-trans ; β-refl ; Lift-Alg-iso ; Lift-Alg-β¨β )
using ( Lift-Alg-assoc ; HomImages ; _IsHomImageOf_ ; Lift-Alg-hom-image )

open  import Base.Subalgebras {π = π}
using ( _β€_ ; _IsSubalgebraOfClass_ ; Subalgebra ; β€-refl ; β-RESP-β€ )
using ( β€-RESP-β ; β€-trans ; Lift-β€-Lift )

```

#### The Inductive Type H

We define the inductive type `H` to represent classes of algebras that include all homomorphic images of algebras in the class; i.e., classes that are closed under the taking of homomorphic images.

```data H{Ξ± Ξ² : Level}(π¦ : Pred(Algebra Ξ± π)(ov Ξ±)) : Pred(Algebra (Ξ± β Ξ²) π)(ov(Ξ± β Ξ²))
where
hbase : {π¨ : Algebra Ξ± π} β π¨ β π¦ β Lift-Alg π¨ Ξ² β H π¦
hhimg : {π¨ π© : Algebra (Ξ± β Ξ²) π} β π¨ β H {Ξ±} {Ξ²} π¦ β ((π© , _) : HomImages π¨) β π© β H π¦
```

#### The Inductive Type S

Here we define the inductive type `S` to represent classes of algebras closed under the taking of subalgebras.

```data S {Ξ± Ξ² : Level}(π¦ : Pred(Algebra Ξ± π)(ov Ξ±)) : Pred(Algebra(Ξ± β Ξ²)π)(ov(Ξ± β Ξ²))
where
sbase : {π¨ : Algebra Ξ± π} β π¨ β π¦ β Lift-Alg π¨ Ξ² β S π¦
slift : {π¨ : Algebra Ξ± π} β π¨ β S{Ξ±}{Ξ±} π¦ β Lift-Alg π¨ Ξ² β S π¦
ssub  : {π¨ : Algebra Ξ± π}{π© : Algebra _ π} β π¨ β S{Ξ±}{Ξ±} π¦ β π© β€ π¨ β π© β S π¦
siso  : {π¨ : Algebra Ξ± π}{π© : Algebra _ π} β π¨ β S{Ξ±}{Ξ±} π¦ β π¨ β π© β π© β S π¦
```

#### The Inductive Type P

Here we define the inductive type `P` to represent classes of algebras closed under the taking of arbitrary products.

```data P {Ξ± Ξ² : Level}(π¦ : Pred(Algebra Ξ± π)(ov Ξ±)) : Pred(Algebra(Ξ± β Ξ²)π)(ov(Ξ± β Ξ²))
where
pbase  : {π¨ : Algebra Ξ± π} β π¨ β π¦ β Lift-Alg π¨ Ξ² β P π¦
pliftu : {π¨ : Algebra Ξ± π} β π¨ β P{Ξ±}{Ξ±} π¦ β Lift-Alg π¨ Ξ² β P π¦
pliftw : {π¨ : Algebra (Ξ± β Ξ²) π} β π¨ β P{Ξ±}{Ξ²} π¦ β Lift-Alg π¨ (Ξ± β Ξ²) β P π¦
produ  : {I : Type Ξ² }{π : I β Algebra Ξ± π} β (β i β (π i) β P{Ξ±}{Ξ±} π¦) β β¨ π β P π¦
prodw  : {I : Type Ξ² }{π : I β Algebra _ π} β (β i β (π i) β P{Ξ±}{Ξ²} π¦) β β¨ π β P π¦
pisow  : {π¨ π© : Algebra _ π} β π¨ β P{Ξ±}{Ξ²} π¦ β π¨ β π© β π© β P π¦
```

#### The Inductive Types V

A class `π¦` of `π`-algebras is called a variety if it is closed under each of the closure operators `H`, `S`, and `P` introduced elsewhere; the corresponding closure operator is often denoted `π`, but we will denote it by `V`.

We now define `V` as an inductive type which is crafted to contain all the parts of `H`, `S` and `P`, under different names.

```data V {Ξ± Ξ² : Level}(π¦ : Pred(Algebra Ξ± π)(ov Ξ±)) : Pred(Algebra(Ξ± β Ξ²)π)(ov(Ξ± β Ξ²))
where
vbase   : {π¨ : Algebra Ξ± π} β π¨ β π¦ β Lift-Alg π¨ Ξ² β V π¦
vlift   : {π¨ : Algebra Ξ± π} β π¨ β V{Ξ±}{Ξ±} π¦ β Lift-Alg π¨ Ξ² β V π¦
vliftw  : {π¨ : Algebra _ π} β π¨ β V{Ξ±}{Ξ²} π¦ β Lift-Alg π¨ (Ξ± β Ξ²) β V π¦
vhimg   : {π¨ π© : Algebra _ π} β π¨ β V{Ξ±}{Ξ²} π¦ β ((π© , _) : HomImages π¨) β π© β V π¦
vssubw  : {π¨ π© : Algebra _ π} β π¨ β V{Ξ±}{Ξ²} π¦ β π© β€ π¨ β π© β V π¦
vprodu  : {I : Type Ξ²}{π : I β Algebra Ξ± π} β (β i β (π i) β V{Ξ±}{Ξ±} π¦) β β¨ π β V π¦
vprodw  : {I : Type Ξ²}{π : I β Algebra _ π} β (β i β (π i) β V{Ξ±}{Ξ²} π¦) β β¨ π β V π¦
visou   : {π¨ : Algebra Ξ± π}{π© : Algebra _ π} β π¨ β V{Ξ±}{Ξ±} π¦ β π¨ β π© β π© β V π¦
visow   : {π¨ π© : Algebra _ π} β π¨ β V{Ξ±}{Ξ²} π¦ β π¨ β π© β π© β V π¦

```

Thus, if π¦ is a class of π-algebras, then the variety generated by π¦ is denoted by `V π¦` and defined to be the smallest class that contains π¦ and is closed under `H`, `S`, and `P`.

With the closure operator V representing closure under HSP, we represent formally what it means to be a variety of algebras as follows.

```is-variety : {Ξ± : Level}(π± : Pred (Algebra Ξ± π)(ov Ξ±)) β Type(ov Ξ±)
is-variety{Ξ±} π± = V{Ξ±}{Ξ±} π± β π±

variety : (Ξ± : Level) β Type(suc (π β π₯ β (suc Ξ±)))
variety Ξ± = Ξ£[ π± β (Pred (Algebra Ξ± π)(ov Ξ±)) ] is-variety π±
```

#### Closure properties of S

`S` is a closure operator. The facts that S is idempotent and expansive wonβt be needed, so we omit these, but we will make use of monotonicity of S. Here is the proof of the latter.

```S-mono :  {Ξ± Ξ² : Level}{π¦ π¦' : Pred (Algebra Ξ± π)(ov Ξ±)}
β        π¦ β π¦' β S{Ξ±}{Ξ²} π¦ β S{Ξ±}{Ξ²} π¦'

S-mono kk (sbase x)            = sbase (kk x)
S-mono kk (slift{π¨} x)         = slift (S-mono kk x)
S-mono kk (ssub{π¨}{π©} sA Bβ€A)  = ssub (S-mono kk sA) Bβ€A
S-mono kk (siso x xβ)          = siso (S-mono kk x) xβ

```

We sometimes want to go back and forth between our two representations of subalgebras of algebras in a class. The tools `subalgebraβS` and `Sβsubalgebra` are made for that purpose.

```module _ {Ξ± Ξ² : Level}{π¦ : Pred (Algebra Ξ± π)(ov Ξ±)} where

subalgebraβS : {π© : Algebra (Ξ± β Ξ²) π} β π© IsSubalgebraOfClass π¦ β π© β S{Ξ±}{Ξ²} π¦
subalgebraβS {π©} (π¨ , ((πͺ , Cβ€A) , KA , BβC)) = ssub sA Bβ€A
where
Bβ€A = β-RESP-β€ {πͺ = π¨} BβC Cβ€A

slAu : Lift-Alg π¨ Ξ± β S{Ξ±}{Ξ±} π¦
slAu = sbase KA

sA : π¨ β S{Ξ±}{Ξ±} π¦
sA = siso slAu (β-sym Lift-β)

module _ {Ξ± : Level}{π¦ : Pred (Algebra Ξ± π)(ov Ξ±)} where

Sβsubalgebra (sbase{π©} x) =  π© , ((π© , (β€-refl β-refl)) , x , β-sym Lift-β)
Sβsubalgebra (slift{π©} x) =  β£ BS β£ ,
SA , β£ snd β₯ BS β₯ β£ , β-trans (β-sym Lift-β) BβSA
where
BS = Sβsubalgebra x
SA : Subalgebra β£ BS β£
SA = fst β₯ BS β₯
BβSA : π© β β£ SA β£
BβSA = β₯ snd β₯ BS β₯ β₯

Sβsubalgebra {π©} (ssub{π¨} sA Bβ€A) = β£ AS β£ , (π© , Bβ€AS) , β£ snd β₯ AS β₯ β£ , β-refl
where
AS : π¨ IsSubalgebraOfClass π¦
AS = Sβsubalgebra sA
SA : Subalgebra β£ AS β£
SA = fst β₯ AS β₯
Bβ€SA : π© β€ β£ SA β£
Bβ€SA = β€-RESP-β Bβ€A (β₯ snd β₯ AS β₯ β₯)
Bβ€AS : π© β€ β£ AS β£
Bβ€AS = β€-trans π© β£ AS β£ Bβ€SA β₯ SA β₯

Sβsubalgebra {π©} (siso{π¨} sA AβB) =  β£ AS β£ ,
SA ,
β£ snd β₯ AS β₯ β£ , (β-trans (β-sym AβB) AβSA)
where
AS : π¨ IsSubalgebraOfClass π¦
AS = Sβsubalgebra sA
SA : Subalgebra β£ AS β£
SA = fst β₯ AS β₯
AβSA : π¨ β β£ SA β£
AβSA = snd β₯ snd AS β₯
```

#### Closure properties of P

`P` is a closure operator. This is proved by checking that `P` is monotone, expansive, and idempotent. The meaning of these terms will be clear from the definitions of the types that follow.

```P-mono :  {Ξ± Ξ² : Level}{π¦ π¦' : Pred(Algebra Ξ± π)(ov Ξ±)}
β        π¦ β π¦' β P{Ξ±}{Ξ²} π¦ β P{Ξ±}{Ξ²} π¦'

P-mono kk' (pbase x)     = pbase (kk' x)
P-mono kk' (pliftu x)    = pliftu (P-mono kk' x)
P-mono kk' (pliftw x)    = pliftw (P-mono kk' x)
P-mono kk' (produ x)     = produ (Ξ» i β P-mono kk' (x i))
P-mono kk' (prodw x)     = prodw (Ξ» i β P-mono kk' (x i))
P-mono kk' (pisow x xβ)  = pisow (P-mono kk' x) xβ

P-expa : {Ξ± : Level}{π¦ : Pred (Algebra Ξ± π)(ov Ξ±)} β π¦ β P{Ξ±}{Ξ±} π¦
P-expa{Ξ±}{π¦} {π¨} KA = pisow {π© = π¨} (pbase KA) (β-sym Lift-β)

module _ {Ξ± Ξ² : Level} where

P-idemp :  {π¦ : Pred (Algebra Ξ± π)(ov Ξ±)}
β         P{Ξ± β Ξ²}{Ξ± β Ξ²} (P{Ξ±}{Ξ± β Ξ²} π¦) β P{Ξ±}{Ξ± β Ξ²} π¦

P-idemp (pbase x)     = pliftw x
P-idemp (pliftu x)    = pliftw (P-idemp x)
P-idemp (pliftw x)    = pliftw (P-idemp x)
P-idemp (produ x)     = prodw (Ξ» i β P-idemp (x i))
P-idemp (prodw x)     = prodw (Ξ» i β P-idemp (x i))
P-idemp (pisow x xβ)  = pisow (P-idemp x) xβ

```

Next we observe that lifting to a higher universe does not break the property of being a subalgebra of an algebra of a class. In other words, if we lift a subalgebra of an algebra in a class, the result is still a subalgebra of an algebra in the class.

```module _ {Ξ± Ξ² : Level}{π¦ : Pred (Algebra Ξ± π)(ov Ξ±)} where

Lift-Alg-subP :  {π© : Algebra Ξ² π}
β               (Lift-Alg π© Ξ±) IsSubalgebraOfClass (P{Ξ±}{Ξ²} π¦)

Lift-Alg-subP (π¨ , (πͺ , Cβ€A) , pA , BβC ) =  lA ,
(lC , lCβ€lA) ,
plA , (Lift-Alg-iso BβC)
where
lA lC : Algebra (Ξ± β Ξ²)  π
lA = Lift-Alg π¨ (Ξ± β Ξ²)
lC = Lift-Alg πͺ Ξ±

lCβ€lA : lC β€ lA
lCβ€lA = Lift-β€-Lift Ξ± {π¨} (Ξ± β Ξ²) Cβ€A
plA : lA β P{Ξ±}{Ξ²} π¦
plA = pliftw pA

Lift-Alg-subP' :  {π¨ : Algebra Ξ± π}
β                π¨ IsSubalgebraOfClass (P{Ξ±}{Ξ±} π¦)
β                (Lift-Alg π¨ Ξ²) IsSubalgebraOfClass (P{Ξ±}{Ξ²} π¦)

Lift-Alg-subP' (π© , (πͺ , Cβ€B) , pB , AβC ) = lB , (lC , lCβ€lB) , plB , (Lift-Alg-iso AβC)
where
lB lC : Algebra (Ξ± β Ξ²)  π
lC = Lift-Alg πͺ Ξ²

lCβ€lB : lC β€ lB
lCβ€lB = Lift-β€-Lift Ξ² {π©} Ξ² Cβ€B
plB : lB β P{Ξ±}{Ξ²} π¦
plB = pliftu pB
```

#### V is closed under lift

As mentioned earlier, a technical hurdle that must be overcome when formalizing proofs in Agda is the proper handling of universe levels. In particular, in the proof of the Birkhoffβs theorem, for example, we will need to know that if an algebra π¨ belongs to the variety V π¦, then so does the lift of π¨. Let us get the tedious proof of this technical lemma out of the way.

```open Level

module Vlift  {Ξ± : Level} {feβ : funext (ov Ξ±) Ξ±}
{feβ : funext ((ov Ξ±) β (suc (ov Ξ±))) (suc (ov Ξ±))}
{feβ : funext (ov Ξ±) (ov Ξ±)}
{π¦ : Pred (Algebra Ξ± π)(ov Ξ±)} where

VlA :  {π¨ : Algebra (ov Ξ±) π} β π¨ β V{Ξ±}{ov Ξ±} π¦
β     Lift-Alg π¨ (suc (ov Ξ±)) β V{Ξ±}{suc (ov Ξ±)} π¦
VlA (vbase{π¨} x) = visow (vbase x) (Lift-Alg-assoc _ _ {π¨})
VlA (vlift{π¨} x) = visow (vlift x) (Lift-Alg-assoc _ _ {π¨})
VlA (vliftw{π¨} x) = visow (VlA x) (Lift-Alg-assoc _ _ {π¨})

VlA (vhimg{π¨}{π©} x hB) = vhimg {π© = Lift-Alg π© (suc (ov Ξ±))} (VlA x) (lC , lChi)
where
lC : Algebra (suc (ov(Ξ±))) π
lC = Lift-Alg β£ hB β£ (suc (ov(Ξ±)))
lChi : lC IsHomImageOf _
lChi = (Lift-Alg-hom-image (suc (ov(Ξ±))) {β£ hB β£} (suc (ov(Ξ±))) β₯ hB β₯)

vssubw (VlA x) (Lift-β€-Lift (suc (ov(Ξ±))) {π¨} (suc (ov(Ξ±))) Bβ€A)

VlA (vprodu{I}{π} x) = visow (vprodw vlA) (β-sym BβA)
where
π° : Type (suc (ov Ξ±))
π° = Lift (suc (ov Ξ±)) I

lA : π° β Algebra (suc (ov Ξ±)) π
lA i = Lift-Alg (π (lower i)) (suc (ov Ξ±))

vlA : β i β (lA i) β V{Ξ±}{suc (ov Ξ±)} π¦
vlA i = vlift (x (lower i))

iso-components : β i β π i β lA (lift i)
iso-components i = Lift-β

BβA : Lift-Alg (β¨ π) (suc (ov Ξ±)) β β¨ lA
BβA = Lift-Alg-β¨β  {fizw = feβ}{fiu = feβ} iso-components

VlA (vprodw{I}{π} x) = visow (vprodw vlA) (β-sym BβA)
where
π° : Type (suc (ov Ξ±))
π° = Lift (suc (ov Ξ±)) I

lA : π° β Algebra (suc (ov Ξ±)) π
lA i = Lift-Alg (π (lower i)) (suc (ov Ξ±))

vlA : β i β (lA i) β V{Ξ±}{suc (ov Ξ±)} π¦
vlA i = VlA (x (lower i))

iso-components : β i β π i β lA (lift i)
iso-components i = Lift-β

BβA : Lift-Alg (β¨ π) (suc (ov Ξ±)) β β¨ lA
BβA = Lift-Alg-β¨β {fizw = feβ}{fiu = feβ} iso-components

VlA (visou{π¨}{π©} x AβB) = visow (vlift x) (Lift-Alg-iso AβB)
VlA (visow{π¨}{π©} x AβB) = visow (VlA x) (Lift-Alg-iso AβB)
```