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

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 : 𝑩 ≀ 𝑨
   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 : {𝑩 : Algebra 𝓀 𝑆} β†’ 𝑩 ∈ S{𝓀}{𝓀} 𝒦  β†’  𝑩 IsSubalgebraOfClass 𝒦

 Sβ†’subalgebra (sbase{𝑩} x) = 𝑩 , (𝑩 , ≀-refl) , x , (β‰…-sym Lift-β‰…)
 Sβ†’subalgebra (slift{𝑩} x) = ∣ BS ∣ , SA , ∣ snd βˆ₯ BS βˆ₯ ∣ , β‰…-trans (β‰…-sym Lift-β‰…) Bβ‰…SA
  where
   BS : 𝑩 IsSubalgebraOfClass 𝒦
   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 𝓀 𝑆}
  β†’              𝑩 IsSubalgebraOfClass (P{𝓀}{𝓀} 𝒦)
                 -------------------------------------------------
  β†’              (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

SβŠ†SP {𝓀}{𝓦}{𝒦}{𝑩}(ssub{𝑨} sA B≀A) =
 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

← Varieties.EquationalLogic Varieties.Preservation β†’