Skip to content

Legacy.Base.Varieties.FreeAlgebras

Free Algebras and Birkhoff's Theorem

Legacy notice. This module is part of the frozen Legacy.Base/ tree. The canonical statement and proof of Birkhoff's HSP theorem in agda-algebras now lives in Setoid.Varieties.HSP, designated canonical under issue #259 (M2-4). The proof below is the original bare-types development from v2.x; it relies on function-extensionality, propositional-extensionality, and set-truncation postulates that the canonical Setoid/ proof retires by construction. It is preserved for v2.x downstream-user continuity and historical reference; new work does not land here. See ADR-001 for the rationale of the Setoid-as-canonical migration, and the self-contained pedagogical companion at Demos.HSP for the TYPES 2021 single-file rendition.

This is the Legacy.Base.Varieties.FreeAlgebras module of the Agda Universal Algebra Library.

First we will define the relatively free algebra in a variety, which is the "freest" algebra among (universal for) those algebras that model all identities holding in the variety. Then we give a formal proof of Birkhoff's theorem which says that a variety is an equational class. In other terms, a class 𝒦 of algebras is closed under the operators H, S, and P if and only if 𝒦 is the class of algebras that satisfy some set of identities.

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Level            using ( Level )
open import Overture  using ( π“ž ; π“₯ ; Signature )
module Legacy.Base.Varieties.FreeAlgebras {Ξ± : Level} {𝑆 : Signature π“ž π“₯} where

-- Imports from Agda and the Agda Standard Library ---------------------
open  import Agda.Primitive   using ( _βŠ”_ )renaming  ( Set to Type )
open  import Data.Product     using ( _,_ ; Ξ£-syntax ; _Γ—_ )
                              renaming  ( proj₁ to fst ; projβ‚‚ to snd )
open  import Function         using ( _∘_ )
open  import Level            using ( suc )
open  import Relation.Binary  using ( IsEquivalence ) renaming  ( Rel to BinRel )
open  import Relation.Unary   using ( Pred ; _∈_ ; _βŠ†_ ; ο½›_｝ ; _βˆͺ_ )

open  import Axiom.Extensionality.Propositional
      using () renaming  (Extensionality to funext)
open  import Relation.Binary.PropositionalEquality as ≑
      using ( _≑_ ; module ≑-Reasoning )

-- Imports from the Agda Universal Algebra Library -------------------------------------------
open  import Overture        using ( ∣_∣ ; βˆ₯_βˆ₯ ; _βˆ™_ ; _⁻¹ )
open  import Legacy.Base.Functions  using ( IsSurjective )
open  import Legacy.Base.Relations  using ( kernel ; βŸͺ_⟫ )
open  import Legacy.Base.Equality
      using ( SwellDef ; swelldef ; is-set ; blk-uip ; hfunext ; DFunExt; pred-ext )

open  import Legacy.Base.Algebras {𝑆 = 𝑆}
      using ( Algebra ; Lift-Alg ; compatible;  _Μ‚_ ; ov ; β¨… ; Con; mkcon ; IsCongruence )
open  import Legacy.Base.Homomorphisms {𝑆 = 𝑆}
      using ( hom ; epi ; epiβ†’hom ; kercon ; ker-in-con ; Ο€ker ; ker[_β‡’_]_β†Ύ_ ; ∘-hom )
      using ( β¨…-hom-co ; HomFactor ; HomFactorEpi ; _β‰…_ ; β‰…-refl ; β‰…-sym ; Lift-β‰… )
open  import Legacy.Base.Terms {𝑆 = 𝑆}
      using ( Term ; 𝑻 ; free-lift ; lift-hom ; free-unique ; _⟦_⟧ )
      using ( lift-of-epi-is-epi ; comm-hom-term; free-lift-interp )
open  import Legacy.Base.Subalgebras {𝑆 = 𝑆}
      using ( _≀_ ; FirstHomCorollary|Set )

open  import Legacy.Base.Varieties.EquationalLogic {𝑆 = 𝑆}
      using ( _⊫_β‰ˆ_; _⊧_β‰ˆ_; Th; Mod )
open  import Legacy.Base.Varieties.Closure {𝑆 = 𝑆}
      using ( S ; P ; V )
open  import Legacy.Base.Varieties.Preservation {𝑆 = 𝑆}
      using ( module class-products-with-maps ; class-ids-β‡’ ; class-ids ; SPβŠ†V')

open Term ; open S ; open V

𝓕 𝓕⁺ : Level
𝓕 = ov Ξ±
𝓕⁺ = suc (ov Ξ±)    -- (this will be the level of the free algebra)

The free algebra in theory

Recall, we proved in the Legacy.Base.Terms.Basic module that the term algebra 𝑻 X is absolutely free in the class of all 𝑆-structures. In this section, we formalize, for a given class 𝒦 of 𝑆-algebras, the (relatively) free algebra in S(P 𝒦) over X.

We use the next definition to take a free algebra for a class 𝒦 and produce the free algebra in 𝒦. Let Θ(𝒦, 𝑨) := {ΞΈ ∈ Con 𝑨 : 𝑨 / ΞΈ ∈ (S 𝒦)}, and let ψ(𝒦, 𝑨) := β‹‚ Θ(𝒦, 𝑨). (Notice that Θ(𝒦, 𝑨) may be empty, in which case ψ(𝒦, 𝑨) = 1 and then 𝑨 / ψ(𝒦, 𝑨) is trivial.) The free algebra is constructed by applying the definitions of ΞΈ and ψ to the special case in which 𝑨 is the algebra 𝑻 X of 𝑆-terms over X.

Since 𝑻 X is free for (and in) the class of all 𝑆-algebras, it follows that 𝑻 X is free for every class 𝒦 of 𝑆-algebras. Of course, 𝑻 X is not necessarily a member of 𝒦, but if we form the quotient of 𝑻 X modulo the congruence ψ(𝒦, 𝑻 X), which we denote by 𝔽[ X ] := (𝑻 X) / ψ(𝒦, 𝑻 X), then it's not hard to see that 𝔽[ X ] is a subdirect product of the algebras in {(𝑻 𝑋) / ΞΈ}, where ΞΈ ranges over Θ(𝒦, 𝑻 X), so 𝔽[ X ] belongs to SP(𝒦), and must therefore satisfy all identities modeled by all members of 𝒦. Indeed, for each pair p q : 𝑻 X, if 𝒦 ⊧ p β‰ˆ q, then p and q belong to the same ψ(𝒦, 𝑻 X)-class, so p and q are identified in the quotient 𝔽[ X ].

The 𝔽[ X ] that we have just defined is called the free algebra over 𝒦 generated by X and (because of what we just observed) we may say that 𝔽[ X ] is free in SP(𝒦).

Remarks. Since X is not a subset of 𝔽[ X ], technically it doesn't make sense to say "X generates 𝔽[ X ]." But as long as 𝒦 contains a nontrivial algebra, we will have ψ(𝒦, 𝑻 𝑋) ∩ XΒ² β‰  βˆ…, and we can identify X with X / ψ(𝒦, 𝑻 X) which is a subset of 𝔽[ X ].

The free algebra in Agda

Before we attempt to represent the free algebra in Agda we construct the congruence ψ(𝒦, 𝑻 𝑋) described above. First, we represent the congruence relation ψCon, modulo which 𝑻 X yields the relatively free algebra, 𝔽[ X ] := 𝑻 X β•± ψCon. We let ψ be the collection of identities (p, q) satisfied by all subalgebras of algebras in 𝒦.

module _ {X : Type Ξ±}(𝒦 : Pred (Algebra Ξ±) 𝓕) where

 ψ : Pred (∣ 𝑻 X ∣ Γ— ∣ 𝑻 X ∣) 𝓕
 ψ (p , q) = βˆ€(𝑨 : Algebra Ξ±)(sA : 𝑨 ∈ S{Ξ±}{Ξ±} 𝒦)(h : X β†’ ∣ 𝑨 ∣ )
                 β†’  (free-lift 𝑨 h) p ≑ (free-lift 𝑨 h) q

We convert the predicate ψ into a relation by currying.

 ψRel : BinRel ∣ 𝑻 X ∣ 𝓕
 ψRel p q = ψ (p , q)

To express ψRel as a congruence of the term algebra 𝑻 X, we must prove that

  1. ψRel is compatible with the operations of 𝑻 X (which are jsut the terms themselves) and
  2. ψRel it is an equivalence relation.
 open ≑-Reasoning

 ψcompatible : swelldef π“₯ Ξ± β†’ compatible (𝑻 X) ψRel
 ψcompatible wd 𝑓 {p} {q} ψpq 𝑨 sA h = Ξ³
  where
  Ο† : hom (𝑻 X) 𝑨
  Ο† = lift-hom 𝑨 h

  Ξ³ : ∣ Ο† ∣ ((𝑓 Μ‚ 𝑻 X) p) ≑ ∣ Ο† ∣ ((𝑓 Μ‚ 𝑻 X) q)

  Ξ³ = ∣ Ο† ∣ ((𝑓 Μ‚ 𝑻 X) p)  β‰‘βŸ¨ βˆ₯ Ο† βˆ₯ 𝑓 p ⟩
      (𝑓 Μ‚ 𝑨) (∣ Ο† ∣ ∘ p)  β‰‘βŸ¨ wd (𝑓 Μ‚ 𝑨)(∣ Ο† ∣ ∘ p)(∣ Ο† ∣ ∘ q)(Ξ» x β†’ ψpq x 𝑨 sA h) ⟩
      (𝑓 Μ‚ 𝑨) (∣ Ο† ∣ ∘ q)  β‰‘βŸ¨ (βˆ₯ Ο† βˆ₯ 𝑓 q)⁻¹ ⟩
      ∣ Ο† ∣ ((𝑓 Μ‚ 𝑻 X) q)  ∎

 ψIsEquivalence : IsEquivalence ψRel
 ψIsEquivalence = record  { refl = Ξ» 𝑨 sA h β†’ ≑.refl
                          ; sym = Ξ» x 𝑨 sA h β†’ (x 𝑨 sA h)⁻¹
                          ; trans = Ξ» pψq qψr 𝑨 sA h β†’ (pψq 𝑨 sA h) βˆ™ (qψr 𝑨 sA h) }

We have collected all the pieces necessary to express the collection of identities satisfied by all subalgebras of algebras in the class as a congruence relation of the term algebra. We call this congruence ψCon and define it using the Congruence constructor mkcon.

 ψCon : swelldef π“₯ Ξ± β†’ Con (𝑻 X)
 ψCon wd = ψRel , mkcon ψIsEquivalence (ψcompatible wd)

HSP Theorem

To complete the proof of the HSP theorem, it remains to show that Mod X (Th (V 𝒦)) is contained in V 𝒦; that is, every algebra that models the equations in Th (V 𝒦) belongs to V 𝒦. This will prove that V 𝒦 is an equational class. (The converse, that every equational class is a variety was already proved; see the remarks at the end of this module.)

We accomplish this goal by constructing an algebra 𝔽 with the following properties:

  1. 𝔽 ∈ V 𝒦 and

  2. Every 𝑨 ∈ Mod X (Th (V 𝒦)) is a homomorphic image of 𝔽.

We denote by β„­ the product of all subalgebras of algebras in 𝒦, and by homβ„­ the homomorphism from 𝑻 X to β„­ defined as follows: homβ„­ := β¨…-hom-co (𝑻 X) 𝔄 hom𝔄. Here, β¨…-hom-co (defined in the Legacy.Base.Homomorphisms.Properties module) takes the term algebra 𝑻 X, a family {𝔄 : I β†’ Algebra Ξ±} of 𝑆-algebras, and a family hom𝔄 : βˆ€ i β†’ hom (𝑻 X) (𝔄 i) of homomorphisms and constructs the natural homomorphism homβ„­ from 𝑻 X to the product β„­ := β¨… 𝔄. The homomorphism homβ„­ : hom (𝑻 X) (β¨… β„­) is "natural" in the sense that the i-th component of the image of t : Term X under homβ„­ is the image ∣ hom𝔄 i ∣ t of t under the i-th homomorphism hom𝔄 i.

𝔽 ≀ β¨… S(𝒦)

Now we come to a step in our approach to formalizing the HSP theorem that turned out to be more technically challenging than we anticipated. We must prove that the free algebra embeds in the product β„­ of all subalgebras of algebras in the class 𝒦. This is really the only stage in the proof of Birkhoff's theorem that requires the truncation assumption that β„­ be a set (that is, β„­ has the UIP property). We will also need to assume several local function extensionality postulates and, as a result, the next submodule will take as given the parameter fe : (βˆ€ a b β†’ funext a b). This allows us to postulate local function extensionality when and where we need it in the proof. For example, if we want to assume function extensionality at universe levels π“₯ and Ξ±, we simply apply fe to those universes: fe π“₯ Ξ±. (Earlier versions of the library used just a single global function extensionality postulate at the start of most modules, but we have since decided to exchange that elegant but crude option for greater precision and transparency.)

module _ {fe : DFunExt}{wd : SwellDef}{X : Type Ξ±} {𝒦 : Pred (Algebra Ξ±) 𝓕} where
 open class-products-with-maps {X = X}{fe 𝓕 Ξ±}{fe 𝓕⁺ 𝓕⁺}{fe 𝓕 𝓕} 𝒦

We begin by constructing β„­, using the techniques described in the section on products of classes.

 -- β„­ is the product of all subalgebras of algebras in 𝒦.
 β„­ : Algebra 𝓕
 β„­ = β¨… 𝔄'

Observe that the inhabitants of β„­ are maps from β„‘ to {𝔄 i : i ∈ β„‘}. A homomorphism from 𝑻 X to β„­ is obtained as follows.

 homβ„­ : hom (𝑻 X) β„­
 homβ„­ = β¨…-hom-co 𝔄' (fe 𝓕 Ξ±){𝓕}(𝑻 X) Ξ» i β†’ lift-hom (𝔄' i)(snd βˆ₯ i βˆ₯)

The free algebra

As mentioned, the initial version of the agda-algebras library used the free algebra 𝔉 developed above. However, our new, more direct proof uses the algebra 𝔽, which we now define, along with the natural epimorphism epi𝔽 : epi (𝑻 X) 𝔽 from 𝑻 X to 𝔽.

We now define the algebra 𝔽, which plays the role of the free algebra, along with the natural epimorphism epi𝔽 : epi (𝑻 X) 𝔽 from 𝑻 X to 𝔽.

 𝔽 : Algebra 𝓕⁺
 𝔽 = ker[ 𝑻 X β‡’ β„­ ] homβ„­ β†Ύ (wd π“₯ (ov Ξ±))

 epi𝔽 : epi (𝑻 X) 𝔽
 epi𝔽 = Ο€ker (wd π“₯ (ov Ξ±)) {β„­} homβ„­

 hom𝔽 : hom (𝑻 X) 𝔽
 hom𝔽 = epiβ†’hom 𝔽 epi𝔽

 hom𝔽-is-epic : IsSurjective ∣ hom𝔽 ∣
 hom𝔽-is-epic = snd βˆ₯ epi𝔽 βˆ₯

We will need the following facts relating homβ„­, hom𝔽, and ψ.

 ψlemma0 : βˆ€ p q β†’  ∣ homβ„­ ∣ p ≑ ∣ homβ„­ ∣ q  β†’ (p , q) ∈ ψ 𝒦
 ψlemma0 p q phomβ„­q 𝑨 sA h = ≑.cong-app phomβ„­q (𝑨 , sA , h)

 ψlemma0-ap : {𝑨 : Algebra Ξ±}{h : X β†’ ∣ 𝑨 ∣} β†’ 𝑨 ∈ S{Ξ±}{Ξ±} 𝒦
  β†’           kernel ∣ hom𝔽 ∣ βŠ† kernel (free-lift 𝑨 h)

 ψlemma0-ap {𝑨}{h} skA {p , q} x = Ξ³ where

  Ξ½ : ∣ homβ„­ ∣ p ≑ ∣ homβ„­ ∣ q
  Ξ½ = ker-in-con {Ξ± = (ov Ξ±)}{ov Ξ±}{𝑻 X}{wd π“₯ (suc (ov Ξ±))}(kercon (wd π“₯ (ov Ξ±)) {β„­} homβ„­) {p}{q} x

  Ξ³ : (free-lift 𝑨 h) p ≑ (free-lift 𝑨 h) q
  Ξ³ = ((ψlemma0 p q) Ξ½) 𝑨 skA h

We now use ψlemma0-ap to prove that every map h : X β†’ ∣ 𝑨 ∣, from X to a subalgebra 𝑨 ∈ S 𝒦 of 𝒦, lifts to a homomorphism from 𝔽 to 𝑨.

 𝔽-lift-hom : (𝑨 : Algebra Ξ±) β†’ 𝑨 ∈ S{Ξ±}{Ξ±} 𝒦 β†’ (X β†’ ∣ 𝑨 ∣) β†’ hom 𝔽 𝑨
 𝔽-lift-hom 𝑨 skA h = fst(HomFactor (wd π“₯ (suc (ov Ξ±)))  𝑨 (lift-hom 𝑨 h) hom𝔽 (ψlemma0-ap skA) hom𝔽-is-epic)

𝒦 models ψ

The goal of this subsection is to prove that 𝒦 models ψ 𝒦. In other terms, for all pairs (p , q) ∈ Term X Γ— Term X of terms, if (p , q) ∈ ψ 𝒦, then 𝒦 ⊫ p β‰ˆ q.

Next we define the lift of the natural embedding from X into 𝔽. We denote this homomorphism by 𝔑 : hom (𝑻 X) 𝔽 and define it as follows.

 open IsCongruence

 Xβ†ͺ𝔽 : X β†’ ∣ 𝔽 ∣
 Xβ†ͺ𝔽 x = βŸͺ β„Š x ⟫ -- (the implicit relation here is  ⟨ kercon (fe π“₯ 𝓕) β„­ homβ„­ ⟩ )

 𝔑 : hom (𝑻 X) 𝔽
 𝔑 = lift-hom 𝔽 Xβ†ͺ𝔽

It turns out that the homomorphism so defined is equivalent to hom𝔽.

 open ≑-Reasoning

 hom𝔽-is-lift-hom : βˆ€ p β†’ ∣ 𝔑 ∣ p ≑ ∣ hom𝔽 ∣ p
 hom𝔽-is-lift-hom (β„Š x) = ≑.refl
 hom𝔽-is-lift-hom (node 𝑓 𝒕) =
  ∣ 𝔑 ∣ (node 𝑓 𝒕)              β‰‘βŸ¨ βˆ₯ 𝔑 βˆ₯ 𝑓 𝒕 ⟩
  (𝑓 Μ‚ 𝔽)(Ξ» i β†’ ∣ 𝔑 ∣(𝒕 i))     β‰‘βŸ¨ wd-proof ⟩
  (𝑓 Μ‚ 𝔽)(Ξ» i β†’ ∣ hom𝔽 ∣ (𝒕 i)) β‰‘βŸ¨ (βˆ₯ hom𝔽 βˆ₯ 𝑓 𝒕)⁻¹ ⟩
  ∣ hom𝔽 ∣ (node 𝑓 𝒕)           ∎
   where wd-proof = wd π“₯ (suc (ov Ξ±))
                    (𝑓 Μ‚ 𝔽) (Ξ» i β†’ ∣ 𝔑 ∣(𝒕 i)) (Ξ» i β†’ ∣ hom𝔽 ∣ (𝒕 i))
                    (Ξ» x β†’ hom𝔽-is-lift-hom(𝒕 x))

We need a three more lemmas before we are ready to tackle our main goal.

 ψlemma1 : kernel ∣ 𝔑 ∣ βŠ† ψ 𝒦
 ψlemma1 {p , q} 𝔑pq 𝑨 sA h = Ξ³
  where
   f : hom 𝔽 𝑨
   f = 𝔽-lift-hom 𝑨 sA h

   h' Ο† : hom (𝑻 X) 𝑨
   h' = ∘-hom (𝑻 X) 𝑨 𝔑 f
   Ο† = lift-hom 𝑨 h

   h≑φ : βˆ€ t β†’ (∣ f ∣ ∘ ∣ 𝔑 ∣) t ≑ ∣ Ο† ∣ t
   h≑φ t = free-unique (wd π“₯ Ξ±) 𝑨 h' Ο† (Ξ» x β†’ ≑.refl) t

   Ξ³ : ∣ Ο† ∣ p ≑ ∣ Ο† ∣ q
   Ξ³ = ∣ Ο† ∣ p             β‰‘βŸ¨ (h≑φ p)⁻¹ ⟩
       ∣ f ∣ ( ∣ 𝔑 ∣ p )   β‰‘βŸ¨ ≑.cong ∣ f ∣ 𝔑pq ⟩
       ∣ f ∣ ( ∣ 𝔑 ∣ q )   β‰‘βŸ¨ h≑φ q ⟩
       ∣ Ο† ∣ q             ∎


 ψlemma2 : kernel ∣ hom𝔽 ∣ βŠ† ψ 𝒦
 ψlemma2 {p , q} x = ψlemma1 {p , q} γ
   where
    Ξ³ : (free-lift 𝔽 Xβ†ͺ𝔽) p ≑ (free-lift 𝔽 Xβ†ͺ𝔽) q
    Ξ³ = (hom𝔽-is-lift-hom p) βˆ™ x βˆ™ (hom𝔽-is-lift-hom q)⁻¹


 ψlemma3 : βˆ€ p q β†’ (p , q) ∈ ψ{X = X} 𝒦 β†’ 𝒦 ⊫ p β‰ˆ q
 ψlemma3 p q pψq {𝑨} kA h = goal
   where
   goal : (𝑨 ⟦ p ⟧) h ≑ (𝑨 ⟦ q ⟧) h
   goal = (𝑨 ⟦ p ⟧) h       β‰‘βŸ¨ free-lift-interp (wd π“₯ Ξ±) 𝑨 h p ⟩
          (free-lift 𝑨 h) p β‰‘βŸ¨ pψq 𝑨 (siso (sbase kA) (β‰…-sym Lift-β‰…)) h ⟩
          (free-lift 𝑨 h) q β‰‘βŸ¨ (free-lift-interp (wd π“₯ Ξ±) 𝑨 h q)⁻¹  ⟩
          (𝑨 ⟦ q ⟧) h       ∎

With these results in hand, it is now trivial to prove the main theorem of this subsection.

 class-models-kernel : βˆ€ p q β†’ (p , q) ∈ kernel ∣ hom𝔽 ∣ β†’ 𝒦 ⊫ p β‰ˆ q
 class-models-kernel p q x = ψlemma3 p q (ψlemma2 x)

 𝕍𝒦 : Pred (Algebra 𝓕⁺) (suc 𝓕⁺)
 𝕍𝒦 = V{Ξ± = Ξ±}{Ξ² = 𝓕⁺} 𝒦

 kernel-in-theory' : kernel ∣ hom𝔽 ∣ βŠ† Th (V 𝒦)
 kernel-in-theory' {p , q} pKq = (class-ids-β‡’ fe wd p q (class-models-kernel p q pKq))

 kernel-in-theory : kernel ∣ hom𝔽 ∣ βŠ† Th 𝕍𝒦
 kernel-in-theory {p , q} pKq vkA x = class-ids fe wd p q (class-models-kernel p q pKq) vkA x

 _β† _ : Type Ξ± β†’ Algebra 𝓕⁺ β†’ Type 𝓕⁺
 X β†  𝑨 = Ξ£[ h ∈ (X β†’ ∣ 𝑨 ∣) ] IsSurjective h

 𝔽-ModTh-epi : (𝑨 : Algebra 𝓕⁺) β†’ (X β†  𝑨) β†’ 𝑨 ∈ Mod (Th 𝕍𝒦) β†’ epi 𝔽 𝑨
 𝔽-ModTh-epi 𝑨 (Ξ· , Ξ·E) AinMTV = goal
  where
  Ο† : hom (𝑻 X) 𝑨
  Ο† = lift-hom 𝑨 Ξ·

  Ο†E : IsSurjective ∣ Ο† ∣
  Ο†E = lift-of-epi-is-epi 𝑨 Ξ·E

  pqlem2 : βˆ€ p q β†’ (p , q) ∈ kernel ∣ hom𝔽 ∣ β†’ 𝑨 ⊧ p β‰ˆ q
  pqlem2 p q z = Ξ» x β†’ AinMTV p q (kernel-in-theory z) x

  kerincl : kernel ∣ hom𝔽 ∣ βŠ† kernel ∣ Ο† ∣
  kerincl {p , q} x = ∣ Ο† ∣ p      β‰‘βŸ¨ (free-lift-interp (wd π“₯ 𝓕⁺) 𝑨 Ξ· p)⁻¹ ⟩
                      (𝑨 ⟦ p ⟧) Ξ·  β‰‘βŸ¨ pqlem2 p q x Ξ· ⟩
                      (𝑨 ⟦ q ⟧) Ξ·  β‰‘βŸ¨ free-lift-interp (wd π“₯ 𝓕⁺) 𝑨 Ξ· q ⟩
                      ∣ Ο† ∣ q      ∎

  goal : epi 𝔽 𝑨
  goal = fst (HomFactorEpi (wd π“₯ (suc (ov Ξ±))) 𝑨 Ο† hom𝔽 kerincl hom𝔽-is-epic Ο†E)

The homomorphic images of 𝔽

Finally we come to one of the main theorems of this module; it asserts that every algebra in Mod X (Th 𝕍𝒦) is a homomorphic image of 𝔽. We prove this below as the function (or proof object) 𝔽-ModTh-epi. Before that, we prove two auxiliary lemmas.

 module _ (pe : pred-ext (ov Ξ±)(ov Ξ±))(wd : SwellDef) -- extensionality assumptions
          (Cset : is-set ∣ β„­ ∣)                       -- truncation assumptions
          (kuip : blk-uip(Term X)∣ kercon (wd π“₯ (ov Ξ±)){β„­}homβ„­ ∣)
  where

  𝔽≀ℭ : (ker[ 𝑻 X β‡’ β„­ ] homβ„­ β†Ύ (wd π“₯ (ov Ξ±))) ≀ β„­
  𝔽≀ℭ = FirstHomCorollary|Set (𝑻 X) β„­ homβ„­ pe (wd π“₯ (ov Ξ±)) Cset kuip

The last piece we need to prove that every model of Th 𝕍𝒦 is a homomorphic image of 𝔽 is a crucial assumption that is taken for granted throughout informal universal algebra---namely, that our collection X of variable symbols is arbitrarily large and that we have an environment which interprets the variable symbols in every algebra under consideration. In other terms, an environment provides, for every algebra 𝑨, a surjective mapping Ξ· : X β†’ ∣ 𝑨 ∣ from X onto the domain of 𝑨.

We do not assert that for an arbitrary type X such surjective maps exist. Indeed, our X must is quite special to have this property. Later, we will construct such an X, but for now we simply postulate its existence. Note that this assumption that an environment exists is only required in the proof of the theorem 𝔽-ModTh-epi.

𝔽 ∈ V(𝒦)

With this result in hand, along with what we proved earlier---namely, PS(𝒦) βŠ† SP(𝒦) βŠ† HSP(𝒦) ≑ V 𝒦---it is not hard to show that 𝔽 belongs to V 𝒦.

  π”½βˆˆSP : hfunext (ov Ξ±)(ov Ξ±) β†’ 𝔽 ∈ (S{𝓕}{𝓕⁺} (P{Ξ±}{𝓕} 𝒦))
  π”½βˆˆSP hfe = ssub (class-prod-s-∈-sp hfe) 𝔽≀ℭ

  π”½βˆˆπ• : hfunext (ov Ξ±)(ov Ξ±) β†’ 𝔽 ∈ V 𝒦
  π”½βˆˆπ• hfe = SPβŠ†V' {Ξ±}{fe 𝓕 Ξ±}{fe 𝓕⁺ 𝓕⁺}{fe 𝓕 𝓕}{𝒦} (π”½βˆˆSP hfe)

The HSP Theorem

Now that we have all of the necessary ingredients, it is all but trivial to combine them to prove Birkhoff's HSP theorem. (Note that since the proof enlists the help of the 𝔽-ModTh-epi theorem, we must assume an environment exists, which is manifested in the premise βˆ€ 𝑨 β†’ X β†  𝑨.

  Birkhoff : hfunext (ov Ξ±)(ov Ξ±) β†’ (βˆ€ 𝑨 β†’ X β†  𝑨) β†’ Mod (Th (V 𝒦)) βŠ† V 𝒦
  Birkhoff hfe 𝕏 {𝑨} Ξ± = vhimg{𝑩 = 𝑨} (π”½βˆˆπ• hfe) (𝑨 , epiβ†’hom 𝑨 Ο†E , snd βˆ₯ Ο†E βˆ₯)
   where
   Ο†E : epi 𝔽 𝑨
   Ο†E = 𝔽-ModTh-epi 𝑨 (𝕏 𝑨) Ξ±

The converse inclusion, V 𝒦 βŠ† Mod X (Th (V 𝒦)), is a simple consequence of the fact that Mod Th is a closure operator. Nonetheless, completeness demands that we formalize this inclusion as well, however trivial the proof.

  Birkhoff-converse : V{Ξ±}{𝓕} 𝒦 βŠ† Mod{X = X} (Th (V 𝒦))
  Birkhoff-converse Ξ± p q pThq = pThq Ξ±

We have thus proved that every variety is an equational class. Readers familiar with the classical formulation of the Birkhoff HSP theorem, as an "if and only if" result, might worry that we haven't completed the proof. But recall that in the Legacy.Base.Varieties.Preservation module we proved the following identity preservation lemmas:

  • 𝒦 ⊫ p β‰ˆ q β†’ H 𝒦 ⊫ p β‰ˆ q
  • 𝒦 ⊫ p β‰ˆ q β†’ S 𝒦 ⊫ p β‰ˆ q
  • 𝒦 ⊫ p β‰ˆ q β†’ P 𝒦 ⊫ p β‰ˆ q

From these it follows that every equational class is a variety. Thus, our formal proof of Birkhoff's theorem is complete.