Agda UALib β

### The Inductive Types H, S, P, V

This section presents the Varieties.Varieties module of the Agda Universal Algebra Library.

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

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

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

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

```

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

• H π¦ = algebras isomorphic to a homomorphic image of a members 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`.

#### Homomorphic closure

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 {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred (Algebra (π€ β π¦) π)(ov(π€ β π¦))
where
hbase : {π¨ : Algebra π€ π} β π¨ β π¦ β Lift-alg π¨ π¦ β H π¦
hlift : {π¨ : Algebra π€ π} β π¨ β H{π€}{π€} π¦ β Lift-alg π¨ π¦ β H π¦
hhimg : {π¨ π© : Algebra _ π} β π¨ β H{π€}{π¦} π¦ β π© is-hom-image-of π¨ β π© β H π¦
hiso  : {π¨ : Algebra _ π}{π© : Algebra _ π} β π¨ β H{π€}{π€} π¦ β π¨ β π© β π© β H π¦

```

#### Subalgebraic closure

The most useful inductive type that we have found for representing the semantic notion of a class of algebras that is closed under the taking of subalgebras is the following.

```
data S {π€ π¦ : Universe}(π¦ : Pred(Algebra π€ π)(ov π€)) : Pred(Algebra(π€ β π¦)π)(ov(π€ β π¦))
where
sbase : {π¨ : Algebra π€ π} β π¨ β π¦ β Lift-alg π¨ π¦ β S π¦
slift : {π¨ : Algebra π€ π} β π¨ β S{π€}{π€} π¦ β Lift-alg π¨ π¦ β S π¦
ssub  : {π¨ : Algebra π€ π}{π© : Algebra _ π} β π¨ β S{π€}{π€} π¦ β π© β€ π¨ β π© β S π¦
ssubw : {π¨ π© : Algebra _ π} β π¨ β S{π€}{π¦} π¦ β π© β€ π¨ β π© β S π¦
siso  : {π¨ : Algebra π€ π}{π© : Algebra _ π} β π¨ β S{π€}{π€} π¦ β π¨ β π© β π© β S π¦

```

#### Product closure

The most useful inductive type that we have found for representing the semantic notion of an class of algebras closed under the taking of arbitrary products is the following.

```
data P {π€ π¦ : Universe}(π¦ : 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 : π¦ Μ }{π : I β Algebra π€ π} β (β i β (π i) β P{π€}{π€} π¦) β β¨ π β P π¦
prodw  : {I : π¦ Μ }{π : I β Algebra _ π} β (β i β (π i) β P{π€}{π¦} π¦) β β¨ π β P π¦
pisou  : {π¨ : Algebra π€ π}{π© : Algebra _ π} β π¨ β P{π€}{π€} π¦ β π¨ β π© β π© β P π¦
pisow  : {π¨ π© : Algebra _ π} β π¨ β P{π€}{π¦} π¦ β π¨ β π© β π© β P π¦

```

#### Varietal closure

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

We now define `V` as an inductive type.

```
data V {π€ π¦ : Universe}(π¦ : 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{π€}{π¦} π¦ β π© is-hom-image-of π¨ β π© β V π¦
vssub  : {π¨ : Algebra π€ π}{π© : Algebra _ π} β π¨ β V{π€}{π€} π¦ β π© β€ π¨ β π© β V π¦
vssubw : {π¨ π© : Algebra _ π} β π¨ β V{π€}{π¦} π¦ β π© β€ π¨ β π© β V π¦
vprodu : {I : π¦ Μ}{π : I β Algebra π€ π} β (β i β (π i) β V{π€}{π€} π¦) β β¨ π β V π¦
vprodw : {I : π¦ Μ}{π : 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 : {π€ : Universe}(π± : Pred (Algebra π€ π)(ov π€)) β ov π€ Μ
is-variety{π€} π± = V{π€}{π€} π± β π±

variety : (π€ : Universe) β (ov π€)βΊ Μ
variety π€ = Ξ£ π± κ (Pred (Algebra π€ π)(ov π€)) , is-variety π±

```

#### Closure properties

The types defined above represent operators with useful closure properties. We now prove a handful of such properties that we need later.

First, `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 : {π€ π¦ : Universe}{π¦ π¦' : 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' (pisou x xβ) = pisou (P-mono kk' x) xβ
P-mono kk' (pisow x xβ) = pisow (P-mono kk' x) xβ

P-expa : {π€ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} β π¦ β P{π€}{π€} π¦
P-expa{π€}{π¦} {π¨} KA = pisou{π¨ = (Lift-alg π¨ π€)}{π© = π¨} (pbase KA) (β-sym Lift-β)

module _ {π€ π¦ : Universe} 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 (pisou x xβ) = pisow (P-idemp x) xβ
P-idemp (pisow x xβ) = pisow (P-idemp x) xβ

```

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

```
S-mono : {π€ π¦ : Universe}{π¦ π¦' : 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' (ssubw{π¨}{π©} sA Bβ€A) = ssubw (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 _ {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} where

subalgebraβS : {π© : Algebra (π€ β π¦) π} β π© IsSubalgebraOfClass π¦ β π© β S{π€}{π¦} π¦

subalgebraβS {π©} (π¨ , ((πͺ , Cβ€A) , KA , BβC)) = ssub sA Bβ€A
where
Bβ€A = β€-iso π¨ BβC Cβ€A

slAu : Lift-alg π¨ π€ β S{π€}{π€} π¦
slAu = sbase KA

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

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

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 = β€-TRANS-β π© β£ SA β£ Bβ€A (β₯ snd β₯ AS β₯ β₯)
Bβ€AS : π© β€ β£ AS β£
Bβ€AS = β€-trans β£ AS β£ Bβ€SA β₯ SA β₯

Sβsubalgebra {π©} (ssubw{π¨} 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 = β€-TRANS-β π© β£ SA β£ 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 β₯

```

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 _ {π€ π¦ : Universe}{π¦ : 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 = pliftu pA

```

The next lemma would be too obvious to care about were it not for the fact that weβll need it later, so it too must be formalized.

```
SβSP : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)}
β     S{π€}{π¦} π¦ β S{π€ β π¦}{π€ β π¦} (P{π€}{π¦} π¦)

SβSP {π€}{π¦}{π¦}{.(Lift-alg π¨ π¦)}(sbase{π¨} x) = siso spllA(β-sym Lift-β)
where
llA : Algebra (π€ β π¦) π
llA = Lift-alg (Lift-alg π¨ π¦) (π€ β π¦)

spllA : llA β S (P π¦)
spllA = sbase{π€ β π¦}{π€ β π¦} (pbase x)

SβSP {π€}{π¦}{π¦} {.(Lift-alg π¨ π¦)} (slift{π¨} x) = subalgebraβS lAsc
where
splAu : π¨ β S(P π¦)
splAu = SβSP{π€}{π€} x

Asc : π¨ IsSubalgebraOfClass (P π¦)
Asc = Sβsubalgebra{π€}{P{π€}{π€} π¦}{π¨} splAu

lAsc : (Lift-alg π¨ π¦) IsSubalgebraOfClass (P π¦)
lAsc = Lift-alg-subP Asc

ssub (subalgebraβS lAsc)( β€-Lift π¨ Bβ€A )
where
lA : Algebra (π€ β π¦) π
lA = Lift-alg π¨ π¦

splAu : π¨ β S (P π¦)
splAu = SβSP{π€}{π€} sA

Asc : π¨ IsSubalgebraOfClass (P π¦)
Asc = Sβsubalgebra{π€}{P{π€}{π€} π¦}{π¨} splAu

lAsc : lA IsSubalgebraOfClass (P π¦)
lAsc = Lift-alg-subP Asc

SβSP (ssubw{π¨} sA Bβ€A) = ssubw (SβSP sA) Bβ€A

SβSP {π€}{π¦}{π¦}{π©}(siso{π¨} sA AβB) = siso{π€ β π¦}{π€ β π¦} lAsp lAβB
where
lA : Algebra (π€ β π¦) π
lA = Lift-alg π¨ π¦

lAsc : lA IsSubalgebraOfClass (P π¦)
lAsc = Lift-alg-subP (Sβsubalgebra{π€}{P{π€}{π€} π¦}{π¨} (SβSP sA))

lAsp : lA β S(P π¦)
lAsp = subalgebraβS{π€ β π¦}{π€ β π¦}{P{π€}{π¦} π¦}{lA} lAsc

lAβB : lA β π©
lAβB = β-trans (β-sym Lift-β) AβB

```

We need to formalize one more lemma before arriving the main objective of this section, which is the proof of the inclusion PSβSP.

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

lemPSβSP : hfunext π¦ π€ β dfunext π¦ π€ β {I : π¦ Μ}{β¬ : I β Algebra π€ π}
β         (β i β (β¬ i) IsSubalgebraOfClass π¦)
-------------------------------------
β         β¨ β¬ IsSubalgebraOfClass (P{π€}{π¦} π¦)

lemPSβSP hfeπ¦π€ feπ¦π€ {I}{β¬} Bβ€K = β¨ π , (β¨ SA , β¨SAβ€β¨π) , ΞΎ , (β¨β {feππ€ = feπ¦π€}{feππ¦ = feπ¦π€} BβSA)
where
π : I β Algebra π€ π
π = Ξ» i β β£ Bβ€K i β£

SA : I β Algebra π€ π
SA = Ξ» i β β£ fst β₯ Bβ€K i β₯ β£

BβSA : β i β β¬ i β SA i
BβSA = Ξ» i β β₯ snd β₯ Bβ€K i β₯ β₯

SAβ€π : β i β (SA i) IsSubalgebraOf (π i)
SAβ€π = Ξ» i β snd β£ β₯ Bβ€K i β₯ β£

h : β i β β£ SA i β£ β β£ π i β£
h = Ξ» i β fst β£ SAβ€π i β£

Ξ± : β£ β¨ SA β£ β β£ β¨ π β£
Ξ± = Ξ» x i β (h i) (x i)
Ξ² : is-homomorphism (β¨ SA) (β¨ π) Ξ±
Ξ² = Ξ» π π β feπ¦π€ Ξ» i β (snd β£ SAβ€π i β£) π (Ξ» x β π x i)
Ξ³ : is-embedding Ξ±
Ξ³ = embedding-lift hfeπ¦π€ hfeπ¦π€ {I}{SA}{π}h(Ξ» i β β₯ SAβ€π i β₯)

β¨SAβ€β¨π : β¨ SA β€ β¨ π
β¨SAβ€β¨π = (Ξ± , Ξ²) , Ξ³

ΞΎ : β¨ π β P π¦
ΞΎ = produ (Ξ» i β P-expa (β£ snd β₯ Bβ€K i β₯ β£))

```

#### PS(π¦) β SP(π¦)

Finally, we are in a position to prove that a product of subalgebras of algebras in a class π¦ is a subalgebra of a product of algebras in π¦.

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

PSβSP : -- extensionality assumptions:
hfunext (ov π€)(ov π€)

β      P{ov π€}{ov π€} (S{π€}{ov π€} π¦) β S{ov π€}{ov π€} (P{π€}{ov π€} π¦)

PSβSP _ (pbase (sbase x)) = sbase (pbase x)
PSβSP _ (pbase (slift{π¨} x)) = slift (SβSP{π€}{ov π€}{π¦} (slift x))
PSβSP _ (pbase{π©}(ssub{π¨} sA Bβ€A)) = siso(ssub(SβSP(slift sA))(Lift-β€-Lift π¨ Bβ€A)) β-refl
PSβSP _ (pbase {π©}(ssubw{π¨} sA Bβ€A)) = ssub(slift(SβSP sA))(Lift-β€-Lift π¨ Bβ€A)
PSβSP _ (pbase (siso{π¨}{π©} x AβB)) = siso (SβSP (slift x)) ( Lift-alg-iso AβB )
PSβSP hfe (pliftu x) = slift (PSβSP hfe x)
PSβSP hfe (pliftw x) = slift (PSβSP hfe x)

PSβSP hfe (produ{I}{π} x) = (S-mono (P-idemp)) (subalgebraβS Ξ·)
where
ΞΎ : (i : I) β (π i) IsSubalgebraOfClass (P{π€}{ov π€} π¦)
ΞΎ i = Sβsubalgebra (PSβSP hfe (x i))

Ξ· : β¨ π IsSubalgebraOfClass (P{ov π€}{ov π€} (P{π€}{ov π€} π¦))
Ξ· = lemPSβSP hfe fovu {I} {π} ΞΎ

PSβSP hfe (prodw{I}{π} x) = (S-mono (P-idemp)) (subalgebraβS Ξ·)
where
ΞΎ : (i : I) β (π i) IsSubalgebraOfClass (P{π€}{ov π€} π¦)
ΞΎ i = Sβsubalgebra (PSβSP hfe (x i))

Ξ· : β¨ π IsSubalgebraOfClass (P{ov π€}{ov π€} (P{π€}{ov π€} π¦))
Ξ· = lemPSβSP hfe fovu  {I} {π} ΞΎ

PSβSP hfe (pisou{π¨}{π©} pA AβB) = siso (PSβSP hfe pA) AβB
PSβSP hfe (pisow{π¨}{π©} pA AβB) = siso (PSβSP hfe pA) AβB

```

#### More class inclusions

We conclude this subsection with three more inclusion relations that will have bit parts to play later (e.g., in the formal proof of Birkhoffβs Theorem).

```
PβV : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)} β P{π€}{π¦} π¦ β V{π€}{π¦} π¦

PβV (pbase x) = vbase x
PβV{π€} (pliftu x) = vlift (PβV{π€}{π€} x)
PβV{π€}{π¦} (pliftw x) = vliftw (PβV{π€}{π¦} x)
PβV (produ x) = vprodu (Ξ» i β PβV (x i))
PβV (prodw x) = vprodw (Ξ» i β PβV (x i))
PβV (pisou x xβ) = visou (PβV x) xβ
PβV (pisow x xβ) = visow (PβV x) xβ

SPβV : {π€ π¦ : Universe}{π¦ : Pred (Algebra π€ π)(ov π€)}
β     S{π€ β π¦}{π€ β π¦} (P{π€}{π¦} π¦) β V π¦

SPβV (sbase{π¨} PCloA) = PβV (pisow PCloA Lift-β)
SPβV (slift{π¨} x) = vliftw (SPβV x)
SPβV (ssub{π¨}{π©} spA Bβ€A) = vssubw (SPβV spA) Bβ€A
SPβV (ssubw{π¨}{π©} spA Bβ€A) = vssubw (SPβV spA) Bβ€A
SPβV (siso x xβ) = visow (SPβV x) xβ

```

#### 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 Lift

module Vlift {feβ : dfunext (ov π€) π€}
{feβ : dfunext ((ov π€) β ((ov π€)βΊ)) ((ov π€) βΊ)}
{feβ : dfunext (ov π€) (ov π€)}
{π¦ : Pred (Algebra π€ π)(ov π€)} where

VlA : {π¨ : Algebra (ov π€) π} β π¨ β V{π€}{ov π€} π¦
β    Lift-alg π¨ (ov π€ βΊ) β V{π€}{ov π€ βΊ} π¦

VlA (vbase{π¨} x) = visow (vbase x) (Lift-alg-associative π¨)
VlA (vlift{π¨} x) = visow (vlift x) (Lift-alg-associative π¨)
VlA (vliftw{π¨} x) = visow (VlA x) (Lift-alg-associative π¨)
VlA (vhimg{π¨}{π©} x hB) = vhimg (VlA x) (Lift-alg-hom-image hB)
VlA (vssub{π¨}{π©} x Bβ€A) = vssubw (vlift{π¦ = (ov π€ βΊ)} x) (Lift-β€-Lift π¨ Bβ€A)
VlA (vssubw{π¨}{π©} x Bβ€A) = vssubw (VlA x) (Lift-β€-Lift π¨ Bβ€A)
VlA (vprodu{I}{π} x) = visow (vprodw vlA) (β-sym BβA)
where
π° : (ov π€ βΊ) Μ
π° = Lift I

lA : π° β Algebra (ov π€ βΊ) π
lA i = Lift-alg (π (lower i)) (ov π€ βΊ)

vlA : β i β (lA i) β V{π€}{ov π€ βΊ} π¦
vlA i = vlift (x (lower i))

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

BβA : Lift-alg (β¨ π) (ov π€ βΊ) β β¨ lA
BβA = Lift-alg-β¨β  {fizw = feβ}{fiu = feβ} iso-components

VlA (vprodw{I}{π} x) = visow (vprodw vlA) (β-sym BβA)
where
π° : (ov π€ βΊ) Μ
π° = Lift I

lA : π° β Algebra (ov π€ βΊ) π
lA i = Lift-alg (π (lower i)) (ov π€ βΊ)

vlA : β i β (lA i) β V{π€}{ov π€ βΊ} π¦
vlA i = VlA (x (lower i))

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

BβA : Lift-alg (β¨ π) (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)

```

Above we proved that `SP(π¦) β V(π¦)`, and we did so under fairly general assumptions about the universe level parameters. Unfortunately, this is sometimes not quite general enough, so we now prove the inclusion again for the specific universe parameters that align with subsequent applications of this result.

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

SPβV' : S{ov π€}{ov π€ βΊ} (P{π€}{ov π€} π¦) β V π¦

SPβV' (sbase{π¨} x) = visow (VlA (SPβV (sbase x))) (β-sym (Lift-alg-associative π¨))
SPβV' (slift x) = VlA (SPβV x)

SPβV' (ssub{π¨}{π©} spA Bβ€A) = vssubw (VlA (SPβV spA)) Bβ€lA
where
Bβ€lA : π© β€ Lift-alg π¨ (ov π€ βΊ)
Bβ€lA = β€-Lift π¨ Bβ€A

SPβV' (ssubw spA Bβ€A) = vssubw (SPβV' spA) Bβ€A

SPβV' (siso{π¨}{π©} x AβB) = visow (VlA (SPβV x)) Ξ³
where
Ξ³ : Lift-alg π¨ (ov π€ βΊ) β π©
Ξ³ = β-trans (β-sym Lift-β) AβB

```

#### β¨ S(π¦) β SP(π¦)

Finally, we prove a result that plays an important role, e.g., in the formal proof of Birkhoffβs Theorem. As we saw in Algebras.Products, the (informal) product `β¨ S(π¦)` of all subalgebras of algebras in π¦ is implemented (formally) in the UALib as `β¨ π S(π¦)`. Our goal is to prove that this product belongs to `SP(π¦)`. We do so by first proving that the product belongs to `PS(π¦)` and then applying the `PSβSP` lemma.

Before doing so, we need to redefine the class product so that each factor comes with a map from the type `X` of variable symbols into that factor. We will explain the reason for this below.

```
module class-products-with-maps
{X : π€ Μ}
{feππ€ : dfunext (ov π€) π€}
{feβ : dfunext ((ov π€) β ((ov π€)βΊ)) ((ov π€) βΊ)}
{feβ : dfunext (ov π€) (ov π€)}
(π¦ : Pred (Algebra π€ π)(ov π€))
where

β : ov π€ Μ
β = Ξ£ π¨ κ (Algebra π€ π) , (π¨ β S{π€}{π€} π¦) Γ (X β β£ π¨ β£)

```

Notice that the second component of this dependent pair type is `(π¨ β π¦) Γ (X β β£ π¨ β£)`. In previous versions of the UALib this second component was simply `π¨ β π¦`, until we realized that adding the type `X β β£ π¨ β£` is quite useful. Later we will see exactly why, but for now suffice it to say that a map of type `X β β£ π¨ β£` may be viewed abstractly as an ambient context, or more concretely, as an assignment of values in `β£ π¨ β£` to variable symbols in `X`. When computing with or reasoning about products, while we donβt want to rigidly impose a context in advance, want do want to lay our hands on whatever context is ultimately assumed. Including the βcontext mapβ inside the index type `β` of the product turns out to be a convenient way to achieve this flexibility.

Taking the product over the index type β requires a function that maps an index `i : β` to the corresponding algebra. Each `i : β` is a triple, say, `(π¨ , p , h)`, where `π¨ : Algebra π€ π`, `p : π¨ β π¦`, and `h : X β β£ π¨ β£`, so the function mapping an index to the corresponding algebra is simply the first projection.

```
π : β β Algebra π€ π
π = Ξ» (i : β) β β£ i β£

```

Finally, we define `class-product` which represents the product of all members of π¦.

```
class-product : Algebra (ov π€) π
class-product = β¨ π

```

If `p : π¨ β π¦` and `h : X β β£ π¨ β£`, we view the triple `(π¨ , p , h) β β` as an index over the class, and so we can think of `π (π¨ , p , h)` (which is simply `π¨`) as the projection of the product `β¨ π` onto the `(π¨ , p, h)`-th component.

```
class-prod-s-β-ps : class-product β P{ov π€}{ov π€}(S π¦)
class-prod-s-β-ps = pisou psPllA (β¨β {feππ€ = feβ}{feππ¦ = feππ€} llAβA) --

where
lA llA : β β Algebra (ov π€) π
lA i =  Lift-alg (π i) (ov π€)
llA i = Lift-alg (lA i) (ov π€)

slA : β i β (lA i) β S π¦
slA i = siso (fst β₯ i β₯) Lift-β

psllA : β i β (llA i) β P (S π¦)
psllA i = pbase (slA i)

psPllA : β¨ llA β P (S π¦)
psPllA = produ psllA

llAβA : β i β (llA i) β (π i)
llAβA i = β-trans (β-sym Lift-β)(β-sym Lift-β)

```

So, since `PSβSP`, we see that that the product of all subalgebras of a class `π¦` belongs to `SP(π¦)`.

```
class-prod-s-β-sp : hfunext (ov π€) (ov π€) β class-product β S(P π¦)
class-prod-s-β-sp hfe = PSβSP {fovu = feβ} hfe class-prod-s-β-ps

```