The Agda Universal Algebra Library (agda-algebras) formalizes the foundations of universal algebra in intensional Martin-Löf type theory (MLTT) using Agda () [@Norell:2007; @agdaref]. The library includes a collection of definitions and verified theorems originated in classical (set-theory based) universal algebra and equational logic, but adapted to MLTT.
The first major milestone of the project is a complete formalization of Birkhoff’s variety theorem (also known as the HSP theorem) [@Birkhoff:1935]. To the best of our knowledge, this is the first time Birkhoff’s celebrated 1935 result has been formalized in MLTT.1
Our first attempt to formalize Birkhoff’s theorem suffered from two flaws.2 First, we
assumed function extensionality in MLTT; consequently, it was unclear whether the
formalization was fully constructive. Second, an inconsistency could be contrived by taking the
type X, representing an arbitrary collection of variable symbols, to be the two element type
(see §7{reference-type=”ref” reference=”sec:discuss”} for details). To resolve
these issues, we developed a new formalization of the HSP theorem based on setoids and
rewrote much of the agda-algebras library to support this approach. This enabled us to
avoid function extensionality altogether. Moreover, the type X of variable symbols was
treated with more care using the context and environment types that Andreas Abel uses
in [@Abel:2021] to formalize Birkhoff’s completeness theorem. These design choices are
discussed further in §2.2{reference-type=”ref”
reference=”setoids”}–2.3{reference-type=”ref”
reference=”setoid-functions”}.
What follows is a self-contained formal proof of the HSP theorem in Agda. This is achieved by extracting a subset of the library, including only the pieces needed for the proof, into a single literate file.3 For spaces reasons, we elide some inessential parts, but strive to preserve the essential content and character of the development. Specifically, routine or overly technical components, as well as anything that does not seem to offer insight into the central ideas of the proof are omitted. (The file [src/Demos/HSP.lagda]{.sans-serif} mentioned above includes the full proof.)
In this paper, we highlight some of the more challenging aspects of formalizing universal algebra in type theory. To some extent, this is a sobering glimpse of the significant technical hurdles that must be overcome to do mathematics in dependent type theory. Nonetheless, we hope to demonstrate that MLTT is a relatively natural language for formalizing universal algebra. Indeed, we believe that researchers with sufficient patience and resolve can reap the substantial rewards of deeper insight and greater confidence in their results by using type theory and a proof assistant like Agda. On the other hand, this paper is probably not the best place to learn about the latter, since we assume the reader is already familiar with MLTT and Agda. In summary, our main contribution is to show that a straightforward but very general representation of algebraic structures in dependent type theory is quite practical, as we demonstrate by formalizing a major seminal result of universal algebra.
To best emulate MLTT, we use
{-# OPTIONS --without-K --exact-split --safe #-}
disables Streicher’s K axiom; directs Agda to accept only definitions behaving like judgmental equalities; safe ensures that nothing is postulated outright. (See [@agdaref-axiomk; @agdaref-safeagda; @agdatools-patternmatching].)
Here are brief descriptions of these options, accompanied by links to related documentation.
without-K disables Streicher’s K axiom. See the section on axiom K in the Agda Language Reference Manual [@agdaref-axiomk].
exact-split directs Agda to accept only definitions behaving like judgmental equalities. See the Pattern matching and equality section of the Agda Tools documentation [@agdatools-patternmatching].
safe ensures that nothing is postulated outright—every non-axiom has to be an explicit assumption (e.g., an argument to a function or module). See the cmdoption-safe section of [@agdaref-safeagda].
We also make use of the following definitions from Agda’s standard library (ver. 1.7).
-- Import universe levels and Signature type (described below) from the agda-algebras library. open import Overture using ( 𝓞 ; 𝓥 ; Signature ) module Demos.HSP {𝑆 : Signature 𝓞 𝓥} where -- Import 16 definitions from the Agda Standard Library. open import Data.Unit.Polymorphic using ( ⊤ ; tt ) open import Function using ( id ; _∘_ ; flip ) open import Level using ( Level ; _⊔_ ; suc ) open import Relation.Binary using ( Rel ; Setoid ; IsEquivalence ; Reflexive ; Symmetric ; Transitive ; Sym ; Trans ) open import Relation.Unary using ( Pred ; _⊆_ ; _∈_ ) open import Relation.Binary.PropositionalEquality using ( _≡_ ) -- Import 23 definitions from the Agda Standard Library and rename 12 of them. 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 () renaming ( Func to _⟶_ ) open _⟶_ using ( cong ) renaming ( f to _⟨$⟩_ ) open IsEquivalence using () renaming ( refl to reflᵉ ; sym to symᵉ ; trans to transᵉ ) open Setoid using ( Carrier ; isEquivalence ) renaming ( _≈_ to _≈ˢ_ ) renaming ( refl to reflˢ ; sym to symˢ ; trans to transˢ ) -- Assign handles to 3 modules of the Agda Standard Library. import Function.Definitions as FD import Relation.Binary.PropositionalEquality as ≡ import Relation.Binary.Reasoning.Setoid as SetoidReasoning private variable α ρᵃ β ρᵇ γ ρᶜ δ ρᵈ ρ χ ℓ : Level Γ Δ : Type χ
The above imports include some adjustments to “standard” Agda syntax; in particular, we use Type in place of Set, the infix long arrow symbol, _⟶_, in place of Func (the type of “setoid functions,” discussed in
§2.3{reference-type=”ref”
reference=”setoid-functions”} below), and the symbol _⟨$⟩_ in place of f (application of the map of a setoid function); we use fst and snd, and sometimes ∣_∣ and ∥_∥, to denote the first and second projections out of the product type _×_.
module _ {A : Type α }{B : A → Type β} where ∣_∣ : Σ[ x ∈ A ] B x → A ∣_∣ = fst ∥_∥ : (z : Σ[ a ∈ A ] B a) → B ∣ z ∣ ∥_∥ = snd
A setoid is a pair consisting of a type and an equivalence relation on that type. Setoids are useful for representing a set with an explicit, “local” notion of equivalence, instead of relying on an implicit, “global” one as is more common in set theory. In reality, informal mathematical practice relies on equivalence relations quite pervasively, taking great care to define only functions that preserve equivalences, while eliding the details. To be properly formal, such details must be made explicit. While there are many different workable approaches, the one that requires no additional meta-theory is based on setoids, which is why we adopt it here. While in some settings setoids are found by others to be burdensome, we have not found them to be so for universal algebra.
The agda-algebras library was first developed without setoids, relying on propositional equality instead, along with some experimental, domain-specific types for equivalence classes, quotients, etc. This required postulating function extensionality,4 which is known to be independent from MLTT [@MHE; @MHE:2019]; this was unsatisfactory as we aimed to show that the theorems hold directly in MLTT without extra axioms. The present work makes no appeal to functional extensionality or classical axioms like Choice or Excluded Middle.5
A setoid function is a function from one setoid to another that respects the underlying equivalences. If [𝑨]{.ab} and [𝑩]{.ab} are setoids, we use [𝑨]{.ab}[⟶]{.aor}[𝑩]{.ab} to denote the type of setoid functions from [𝑨]{.ab} to [𝑩]{.ab}.
An example of a setoid function is the identity function from a setoid to itself. We define it, along with a binary composition operation for setoid functions, _⟨∘⟩_, as follows.
𝑖𝑑 : {A : Setoid α ρᵃ} → A ⟶ A 𝑖𝑑 {A} = record { f = id ; cong = id } _⟨∘⟩_ : {A : Setoid α ρᵃ} {B : Setoid β ρᵇ} {C : Setoid γ ρᶜ} → B ⟶ C → A ⟶ B → A ⟶ C f ⟨∘⟩ g = record { f = (_⟨$⟩_ f) ∘ (_⟨$⟩_ g) ; cong = (cong f) ∘ (cong g) }
We define the inverse of a setoid function in terms of the image of the function’s domain, as follows.
module _ {𝑨 : Setoid α ρᵃ}{𝑩 : Setoid β ρᵇ} where open Setoid 𝑩 using ( _≈_ ; sym ) renaming ( Carrier to B ) data Image_∋_ (f : 𝑨 ⟶ 𝑩) : B → Type (α ⊔ β ⊔ ρᵇ) where eq : {b : B} → ∀ a → b ≈ f ⟨$⟩ a → Image f ∋ b
An inhabitant of the Image f ∋ b type is a point a : Carrier 𝑨, along with a proof p : b ≈ f a, that f maps a to b. Since a proof of Image f ∋ b must include a concrete witness a : Carrier 𝑨, we can actually compute a range-restricted right-inverse of f. Here is the definition of Inv which, for extra
certainty, is accompanied by a proof that it gives such a right-inverse.
Inv : (f : 𝑨 ⟶ 𝑩){b : B} → Image f ∋ b → Carrier 𝑨 Inv _ (eq a _) = a InvIsInverseʳ : {f : 𝑨 ⟶ 𝑩}{b : B}(q : Image f ∋ b) → f ⟨$⟩ (Inv f q) ≈ b InvIsInverseʳ (eq _ p) = sym p
If f : 𝑨 ⟶ 𝑩 then we call f injective provided ∀(a₀ a₁ : A), f ⟨$⟩ a₀ ≈ᴮ f ⟨$⟩ a₁ implies a₀ ≈ᴬ a₁; we call f surjective provided ∀(b : B) ∃(a : A) such that f ⟨$⟩ a ≈ᴮ b.
We represent injective functions on bare types by the type Injective, and use this to define the IsInjective type representing the property of being an injective setoid function. Similarly, the type IsSurjective
represents the property of being a surjective setoid function and SurjInv represents the right-inverse of a surjective function.
We reproduce the definitions and prove some of their properties inside the next submodule where we first set the stage by declaring two setoids 𝑨 and 𝑩 and naming their equality relations.
module _ {𝑨 : Setoid α ρᵃ}{𝑩 : Setoid β ρᵇ} where open Setoid 𝑨 using () renaming ( _≈_ to _≈ᴬ_ ) open Setoid 𝑩 using () renaming ( _≈_ to _≈ᴮ_ ) open FD _≈ᴬ_ _≈ᴮ_ IsInjective : (𝑨 ⟶ 𝑩) → Type (α ⊔ ρᵃ ⊔ ρᵇ) IsInjective f = Injective (_⟨$⟩_ f) IsSurjective : (𝑨 ⟶ 𝑩) → Type (α ⊔ β ⊔ ρᵇ) IsSurjective F = ∀ {y} → Image F ∋ y SurjInv : (f : 𝑨 ⟶ 𝑩) → IsSurjective f → Carrier 𝑩 → Carrier 𝑨 SurjInv f fonto b = Inv f (fonto {b})
Proving that the composition of injective setoid functions is again injective is simply a matter of composing the two assumed witnesses to injectivity. Proving that surjectivity is preserved under composition is only slightly more involved.
module _ {𝑨 : Setoid α ρᵃ}{𝑩 : Setoid β ρᵇ}{𝑪 : Setoid γ ρᶜ} (f : 𝑨 ⟶ 𝑩)(g : 𝑩 ⟶ 𝑪) where ∘-IsInjective : IsInjective f → IsInjective g → IsInjective (g ⟨∘⟩ f) ∘-IsInjective finj ginj = finj ∘ ginj ∘-IsSurjective : IsSurjective f → IsSurjective g → IsSurjective (g ⟨∘⟩ f) ∘-IsSurjective fonto gonto {y} = Goal where mp : Image g ∋ y → Image g ⟨∘⟩ f ∋ y mp (eq c p) = η fonto where open Setoid 𝑪 using ( trans ) η : Image f ∋ c → Image g ⟨∘⟩ f ∋ y η (eq a q) = eq a (trans p (cong g q)) Goal : Image g ⟨∘⟩ f ∋ y Goal = mp gonto
Every (setoid) function f : A ⟶ B factors as a surjective map toIm : A ⟶ Im f followed
by an injective map fromIm : Im f ⟶ B.
module _ {𝑨 : Setoid α ρᵃ}{𝑩 : Setoid β ρᵇ} where Im : (f : 𝑨 ⟶ 𝑩) → Setoid _ _ Carrier (Im f) = Carrier 𝑨 _≈ˢ_ (Im f) b1 b2 = f ⟨$⟩ b1 ≈ f ⟨$⟩ b2 where open Setoid 𝑩 isEquivalence (Im f) = record { refl = refl ; sym = sym; trans = trans } where open Setoid 𝑩 toIm : (f : 𝑨 ⟶ 𝑩) → 𝑨 ⟶ Im f toIm f = record { f = id ; cong = cong f } fromIm : (f : 𝑨 ⟶ 𝑩) → Im f ⟶ 𝑩 fromIm f = record { f = λ x → f ⟨$⟩ x ; cong = id } fromIm-inj : (f : 𝑨 ⟶ 𝑩) → IsInjective (fromIm f) fromIm-inj _ = id toIm-surj : (f : 𝑨 ⟶ 𝑩) → IsSurjective (toIm f) toIm-surj _ = eq _ (reflˢ 𝑩)
We now develop a working vocabulary in MLTT corresponding to classical, single-sorted, set-based universal algebra. We cover a number of important concepts, but limit ourselves to those required to prove Birkhoff’s HSP theorem. In each case, we give a type-theoretic version of the informal definition, followed by its implementation in Agda.
This section is organized into the following subsections: §3.1{reference-type=”ref” reference=”signatures”} defines a general type of signatures of algebraic structures; §3.2{reference-type=”ref” reference=”algebras”} does the same for structures and their products; §3.3{reference-type=”ref” reference=”homomorphisms”} defines homomorphisms, monomorphisms, and epimorphisms, presents types that codify these concepts, and formally verifies some of their basic properties; §3.5{reference-type=”ref” reference=”subalgebras”}–3.6{reference-type=”ref” reference=”terms”} do the same for subalgebras and terms, respectively.
An (algebraic) signature is a pair 𝑆 = (F, ρ) where F is a collection of operation symbols and ρ : F → N is an arity function which maps each operation symbol to its arity. Here, N denotes the arity type. Heuristically, the arity of an operation symbol may be thought of as the number of arguments that takes as
“input.” We represent signatures as inhabitants of the following dependent pair type.
Signature : (𝒪 𝒱 : Level) → Type (lsuc (𝒪 ⊔ 𝒱))
Signature 𝒪 𝒱 = Σ[ F ∈ Type 𝒪 ] (F → Type 𝒱)
Recalling our syntax for the first and second projections, if 𝑆 is a signature, then ∣ 𝑆 ∣ denotes the set of operation symbols and ∥ 𝑆 ∥ denotes the arity function. Thus, if f : ∣ 𝑆 ∣ is an operation symbol in the signature 𝑆, then ∥ 𝑆 ∥ f is the arity of f.
We need to augment our Signature type so that it supports algebras over setoid domains. To do so, following Abel [@Abel:2021], we define an operator that translates an ordinary signature into a setoid signature, that is, a signature over a setoid domain. This raises a minor technical issue: given operations f and g, with arguments u : ∥ 𝑆 ∥ f → A and v : ∥ 𝑆 ∥ g → A, respectively, and a proof of f ≡ g (intensional equality), we ought to be able to check whether u and v are pointwise equal. Technically, u and v appear to inhabit different types; of course, this is reconciled by the hypothesis f ≡ g, as we see in the next definition (borrowed from [@Abel:2021]).
EqArgs : {𝑆 : Signature 𝓞 𝓥}{ξ : Setoid α ρᵃ} → ∀ {f g} → f ≡ g → (∥ 𝑆 ∥ f → Carrier ξ) → (∥ 𝑆 ∥ g → Carrier ξ) → Type (𝓥 ⊔ ρᵃ) EqArgs {ξ = ξ} ≡.refl u v = ∀ i → u i ≈ v i where open Setoid ξ using ( _≈_ )
This makes it possible to define an operator which translates a signature for algebras over bare types into a signature for algebras over setoids. We denote this operator by ⟨_⟩ and define it as follows.
⟨_⟩ : Signature 𝓞 𝓥 → Setoid α ρᵃ → Setoid _ _ Carrier (⟨ 𝑆 ⟩ ξ) = Σ[ f ∈ ∣ 𝑆 ∣ ] (∥ 𝑆 ∥ f → ξ .Carrier) _≈ˢ_ (⟨ 𝑆 ⟩ ξ)(f , u)(g , v) = Σ[ eqv ∈ f ≡ g ] EqArgs{ξ = ξ} eqv u v reflᵉ (isEquivalence (⟨ 𝑆 ⟩ ξ)) = ≡.refl , λ i → reflˢ ξ symᵉ (isEquivalence (⟨ 𝑆 ⟩ ξ)) (≡.refl , g) = ≡.refl , λ i → symˢ ξ (g i) transᵉ (isEquivalence (⟨ 𝑆 ⟩ ξ)) (≡.refl , g)(≡.refl , h) = ≡.refl , λ i → transˢ ξ (g i) (h i)
An algebraic structure 𝑨 = (A, Fᴬ) in the signature 𝑆 = (F, ρ), or 𝑆-algebra, consists of
A, called the domain of the algebra;Fᴬ := {fᴬ ∣ f ∈ F, fᴬ : (ρ f → A) → A} of operations on A;𝑨.
Our Agda implementation represents algebras as inhabitants of a record type with two fields—a Domain setoid denoting the domain of the algebra, and an Interp function denoting the interpretation in the algebra of each operation symbol in 𝑆. We postpone introducing identities until §4{reference-type=”ref” reference=”equational-logic”}.record Algebra α ρ : Type (𝓞 ⊔ 𝓥 ⊔ suc (α ⊔ ρ)) where field Domain : Setoid α ρ Interp : ⟨ 𝑆 ⟩ Domain ⟶ Domain
Thus, for each operation symbol in 𝑆 we have a setoid function f whose domain is a power of Domain and whose codomain is Domain. Further, we define some syntactic sugar to make our formalizations easier to read and reason about. Specifically, if 𝑨 is an algebra, then
𝔻[ 𝑨 ] denotes the Domain setoid of 𝑨,𝕌[ 𝑨 ] is the underlying carrier of (the Domain setoid of) 𝑨, andf ̂ 𝑨 denotes the interpretation of the operation symbol f in the algebra 𝑨.open Algebra 𝔻[_] : Algebra α ρᵃ → Setoid α ρᵃ 𝔻[ 𝑨 ] = Domain 𝑨 𝕌[_] : Algebra α ρᵃ → Type α 𝕌[ 𝑨 ] = Carrier (Domain 𝑨) _̂_ : (f : ∣ 𝑆 ∣)(𝑨 : Algebra α ρᵃ) → (∥ 𝑆 ∥ f → 𝕌[ 𝑨 ]) → 𝕌[ 𝑨 ] f ̂ 𝑨 = λ a → (Interp 𝑨) ⟨$⟩ (f , a)
Types belong to universes, which are structured in Agda as follows:
Type ℓ : Type (suc ℓ), Type (suc ℓ) : Type (suc (suc ℓ)).7
While this means that Type ℓ has type Type (suc ℓ), it does not imply that Type ℓ
has type Type (suc (suc ℓ)). In other words, Agda’s universes are non-cumulative.
This can be advantageous as it becomes possible to treat size issues more generally and precisely.
However, dealing with explicit universe levels can be daunting, and the standard literature
(in which uniform smallness is typically assumed) offers little guidance. While in some settings,
such as category theory, formalizing in Agda works smoothly with respect to universe levels
(see [@agda-categories]), in universal algebra the terrain is bumpier. Thus, it seems worthwhile to
explain how we make use of universe lifting and lowering functions, available in the
Agda Standard Library, to develop domain-specific tools for dealing with Agda’s non-cumulative
universe hierarchy.
The Lift operation of the standard library embeds a type into a higher universe. Specializing Lift to our situation, we define a function Lift-Alg.
module _ (𝑨 : Algebra α ρᵃ) where open Setoid 𝔻[ 𝑨 ] using ( _≈_ ; refl ; sym ; trans ) ; open Level Lift-Algˡ : (ℓ : Level) → Algebra (α ⊔ ℓ) ρᵃ Domain (Lift-Algˡ ℓ) = record { Carrier = Lift ℓ 𝕌[ 𝑨 ] ; _≈_ = λ x y → lower x ≈ lower y ; isEquivalence = record { refl = refl ; sym = sym ; trans = trans } } Interp (Lift-Algˡ ℓ) ⟨$⟩ (f , la) = lift ((f ̂ 𝑨) (lower ∘ la)) cong (Interp (Lift-Algˡ ℓ)) (≡.refl , lab) = cong (Interp 𝑨) ((≡.refl , lab)) Lift-Algʳ : (ℓ : Level) → Algebra α (ρᵃ ⊔ ℓ) Domain (Lift-Algʳ ℓ) = record { Carrier = 𝕌[ 𝑨 ] ; _≈_ = λ x y → Lift ℓ (x ≈ y) ; isEquivalence = record { refl = lift refl ; sym = lift ∘ sym ∘ lower ; trans = λ x y → lift (trans (lower x)(lower y)) } } Interp (Lift-Algʳ ℓ ) ⟨$⟩ (f , la) = (f ̂ 𝑨) la cong (Interp (Lift-Algʳ ℓ))(≡.refl , lab) = lift ( cong (Interp 𝑨) ( ≡.refl , λ i → lower (lab i) ) ) Lift-Alg : Algebra α ρᵃ → (ℓ₀ ℓ₁ : Level) → Algebra (α ⊔ ℓ₀) (ρᵃ ⊔ ℓ₁) Lift-Alg 𝑨 ℓ₀ ℓ₁ = Lift-Algʳ (Lift-Algˡ 𝑨 ℓ₀) ℓ₁
Recall that our Algebra type has two universe level parameters corresponding to
those of the domain setoid. Concretely, an algebra of type Algebra α ρᵃ has a
Domain of type Setoid α ρᵃ. This packages a “carrier set” (Carrier),
inhabiting Type α, with an equality on Carrier of type Rel Carrier ρᵃ.
Lift-Alg takes an algebra parametrized by levels α and ρᵃ and constructs a
new algebra whose carrier inhabits Type (α ⊔ ℓ₀) and whose equivalence inhabits
Rel Carrier (ρᵃ ⊔ ℓ₁). To be useful, this lifting operation should result in an
algebra with the same semantic properties as the one we started with. We will see
in §3.4{reference-type=”ref” reference=”sec:lift-alg”} that this
is indeed the case.
We define the product of a family of algebras as follows. Let ι be a universe
and I : Type ι a type (the “indexing type”). Then 𝒜 : I → Algebra α ρᵃ
represents an indexed family of algebras. Denote by ⨅ 𝒜 the product of
algebras in 𝒜 (or product algebra), by which we mean the algebra whose domain
is the Cartesian product ∏[i ∈ I] 𝔻[ 𝒜 i ] of the domains of the algebras in
𝒜, and whose operations are those arising from the point-wise interpretation of
the operation symbols in the obvious way: if f is a J-ary operation symbol and
if a : Π[ i ∈ I ] J → 𝔻[ 𝒜 i ] is, for each i : I, a J-tuple of elements of
the domain 𝔻[ 𝒜 i ], then we define the interpretation of f in ⨅ 𝒜 by
(f ̂ ⨅ 𝒜) a := λ (i : I) → (f ̂ 𝒜 i)(a i).
Here is the formal definition of the product algebra type in Agda.
module _ {ι : Level}{I : Type ι } where ⨅ : (𝒜 : I → Algebra α ρᵃ) → Algebra (α ⊔ ι) (ρᵃ ⊔ ι) Domain (⨅ 𝒜) = record { Carrier = ∀ i → 𝕌[ 𝒜 i ] ; _≈_ = λ a b → ∀ i → (_≈ˢ_ 𝔻[ 𝒜 i ]) (a i)(b i) ; isEquivalence = record { refl = λ i → reflᵉ (isEquivalence 𝔻[ 𝒜 i ]) ; sym = λ x i → symᵉ (isEquivalence 𝔻[ 𝒜 i ])(x i) ; trans = λ x y i → transᵉ (isEquivalence 𝔻[ 𝒜 i ])(x i)(y i) } } Interp (⨅ 𝒜) ⟨$⟩ (f , a) = λ i → (f ̂ (𝒜 i)) (flip a i) cong (Interp (⨅ 𝒜)) (≡.refl , f=g ) = λ i → cong ( Interp (𝒜 i) ) ( ≡.refl , flip f=g i )
Evidently, the carrier of the product algebra type is indeed the (dependent) product of the carriers in the indexed family. The rest of the definitions are the point-wise versions of the underlying ones.
Throughout the rest of the paper, unless stated otherwise, 𝑨 and 𝑩 will denote
𝑆-algebras inhabiting the types Algebra α ρᵃ and Algebra β ρᵇ, respectively.
A homomorphism (or “hom”) from 𝑨 to 𝑩 is a setoid function
h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ] that is compatible with all basic operations; that is, for
every operation symbol f : ∣ 𝑆 ∣ and all tuples a : ∥ 𝑆 ∥ f → 𝕌[ 𝑨 ], we have
h ⟨$⟩ (f ̂ 𝑨) a ≈ (f ̂ 𝑩) λ x → h ⟨$⟩ (a x).
It is convenient to first formalize “compatible” (compatible-map-op),
representing the assertion that a given setoid function h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]
commutes with a given operation symbol f, and then generalize over operation
symbols to yield the type (compatible-map) of compatible maps from (the domain
of) 𝑨 to (the domain of) 𝑩.
module _ (𝑨 : Algebra α ρᵃ)(𝑩 : Algebra β ρᵇ) where compatible-map-op : (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) → ∣ 𝑆 ∣ → Type _ compatible-map-op h f = ∀ {a} → h ⟨$⟩ (f ̂ 𝑨) a ≈ (f ̂ 𝑩) λ x → h ⟨$⟩ (a x) where open Setoid 𝔻[ 𝑩 ] using ( _≈_ ) compatible-map : (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) → Type _ compatible-map h = ∀ {f} → compatible-map-op h f
Using these we define the property (IsHom) of being a homomorphism, and
finally the type (hom) of homomorphisms from 𝑨 to 𝑩.
record IsHom (h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵇ) where constructor mkhom field compatible : compatible-map h hom : Type _ hom = Σ (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) IsHom
Thus, an inhabitant of hom 𝑨 𝑩 is a pair (h , p) consisting of a setoid
function h, from the domain of 𝑨 to that of 𝑩, along with a proof p that
h is a homomorphism.
A monomorphism (resp. epimorphism) is an injective (resp. surjective) homomorphism. The agda-algebras library defines predicates and for these, as well as and for the corresponding types.
record IsMon (h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ ⊔ ρᵇ) where field isHom : IsHom h isInjective : IsInjective h HomReduct : hom HomReduct = h , isHom mon : Type _ mon = Σ (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) IsMon
As with hom, the type mon is a dependent product type; each inhabitant is a
pair consisting of a setoid function, say, h, along with a proof that h is a
monomorphism.
record IsEpi (h : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ β ⊔ ρᵇ) where field isHom : IsHom h isSurjective : IsSurjective h HomReduct : hom HomReduct = h , isHom epi : Type _ epi = Σ (𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]) IsEpi
Here are two utilities that are useful for translating between types.
open IsHom ; open IsMon ; open IsEpi module _ (𝑨 : Algebra α ρᵃ)(𝑩 : Algebra β ρᵇ) where mon→intohom : mon 𝑨 𝑩 → Σ[ h ∈ hom 𝑨 𝑩 ] IsInjective ∣ h ∣ mon→intohom (hh , hhM) = (hh , isHom hhM) , isInjective hhM epi→ontohom : epi 𝑨 𝑩 → Σ[ h ∈ hom 𝑨 𝑩 ] IsSurjective ∣ h ∣ epi→ontohom (hh , hhE) = (hh , isHom hhE) , isSurjective hhE
The composition of homomorphisms is again a homomorphism, and similarly for epimorphisms and monomorphisms. The proofs of these facts are straightforward.
module _ {𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} {g : 𝔻[ 𝑨 ] ⟶ 𝔻[ 𝑩 ]}{h : 𝔻[ 𝑩 ] ⟶ 𝔻[ 𝑪 ]} where open Setoid 𝔻[ 𝑪 ] using ( trans ) ∘-is-hom : IsHom 𝑨 𝑩 g → IsHom 𝑩 𝑪 h → IsHom 𝑨 𝑪 (h ⟨∘⟩ g) ∘-is-hom ghom hhom = mkhom c where c : compatible-map 𝑨 𝑪 (h ⟨∘⟩ g) c = trans (cong h (compatible ghom)) (compatible hhom) ∘-is-epi : IsEpi 𝑨 𝑩 g → IsEpi 𝑩 𝑪 h → IsEpi 𝑨 𝑪 (h ⟨∘⟩ g) ∘-is-epi gE hE = record { isHom = ∘-is-hom (isHom gE) (isHom hE) ; isSurjective = ∘-IsSurjective g h (isSurjective gE) (isSurjective hE) } module _ {𝑨 : Algebra α ρᵃ} {𝑩 : Algebra β ρᵇ} {𝑪 : Algebra γ ρᶜ} where ∘-hom : hom 𝑨 𝑩 → hom 𝑩 𝑪 → hom 𝑨 𝑪 ∘-hom (h , hhom) (g , ghom) = (g ⟨∘⟩ h) , ∘-is-hom hhom ghom ∘-epi : epi 𝑨 𝑩 → epi 𝑩 𝑪 → epi 𝑨 𝑪 ∘-epi (h , hepi) (g , gepi) = (g ⟨∘⟩ h) , ∘-is-epi hepi gepi
Here we define the identity homomorphism for setoid algebras. Then we prove that the operations of lifting and lowering of a setoid algebra are homomorphisms.
𝒾𝒹 : {𝑨 : Algebra α ρᵃ} → hom 𝑨 𝑨 𝒾𝒹 {𝑨 = 𝑨} = 𝑖𝑑 , mkhom (reflexive ≡.refl) where open Setoid ( Domain 𝑨 ) using ( reflexive ) module _ {𝑨 : Algebra α ρᵃ}{ℓ : Level} where open Setoid 𝔻[ 𝑨 ] using ( reflexive ) renaming ( _≈_ to _≈₁_ ; refl to refl₁ ) open Setoid 𝔻[ Lift-Algˡ 𝑨 ℓ ] using () renaming ( _≈_ to _≈ˡ_ ; refl to reflˡ) open Setoid 𝔻[ Lift-Algʳ 𝑨 ℓ ] using () renaming ( _≈_ to _≈ʳ_ ; refl to reflʳ) open Level ToLiftˡ : hom 𝑨 (Lift-Algˡ 𝑨 ℓ) ToLiftˡ = record { f = lift ; cong = id } , mkhom (reflexive ≡.refl) FromLiftˡ : hom (Lift-Algˡ 𝑨 ℓ) 𝑨 FromLiftˡ = record { f = lower ; cong = id } , mkhom reflˡ ToFromLiftˡ : ∀ b → ∣ ToLiftˡ ∣ ⟨$⟩ (∣ FromLiftˡ ∣ ⟨$⟩ b) ≈ˡ b ToFromLiftˡ b = refl₁ FromToLiftˡ : ∀ a → ∣ FromLiftˡ ∣ ⟨$⟩ (∣ ToLiftˡ ∣ ⟨$⟩ a) ≈₁ a FromToLiftˡ a = refl₁ ToLiftʳ : hom 𝑨 (Lift-Algʳ 𝑨 ℓ) ToLiftʳ = record { f = id ; cong = lift } , mkhom (lift (reflexive ≡.refl)) FromLiftʳ : hom (Lift-Algʳ 𝑨 ℓ) 𝑨 FromLiftʳ = record { f = id ; cong = lower } , mkhom reflˡ ToFromLiftʳ : ∀ b → ∣ ToLiftʳ ∣ ⟨$⟩ (∣ FromLiftʳ ∣ ⟨$⟩ b) ≈ʳ b ToFromLiftʳ b = lift refl₁ FromToLiftʳ : ∀ a → ∣ FromLiftʳ ∣ ⟨$⟩ (∣ ToLiftʳ ∣ ⟨$⟩ a) ≈₁ a FromToLiftʳ a = refl₁ module _ {𝑨 : Algebra α ρᵃ}{ℓ r : Level} where open Setoid 𝔻[ 𝑨 ] using ( refl ) open Setoid 𝔻[ Lift-Alg 𝑨 ℓ r ] using ( _≈_ ) open Level ToLift : hom 𝑨 (Lift-Alg 𝑨 ℓ r) ToLift = ∘-hom ToLiftˡ ToLiftʳ FromLift : hom (Lift-Alg 𝑨 ℓ r) 𝑨 FromLift = ∘-hom FromLiftʳ FromLiftˡ ToFromLift : ∀ b → ∣ ToLift ∣ ⟨$⟩ (∣ FromLift ∣ ⟨$⟩ b) ≈ b ToFromLift b = lift refl ToLift-epi : epi 𝑨 (Lift-Alg 𝑨 ℓ r) ToLift-epi = ∣ ToLift ∣ , record { isHom = ∥ ToLift ∥ ; isSurjective = λ{y} → eq(∣ FromLift ∣ ⟨$⟩ y)(ToFromLift y) }
Suppose we have an algebra 𝑨, a type I : Type 𝓘, and a family
ℬ : I → Algebra β ρᵇ of algebras. We sometimes refer to the inhabitants of I
as indices, and call ℬ an indexed family of algebras. If in addition we have
a family 𝒽 : (i : I) → hom 𝑨 (ℬ i) of homomorphisms, then we can construct a
homomorphism from 𝑨 to the product ⨅ ℬ in the natural way. We codify the
latter in dependent type theory as follows.
module _ {ι : Level}{I : Type ι}{𝑨 : Algebra α ρᵃ}(ℬ : I → Algebra β ρᵇ) where ⨅-hom-co : (∀(i : I) → hom 𝑨 (ℬ i)) → hom 𝑨 (⨅ ℬ) ⨅-hom-co 𝒽 = h , hhom where h : 𝔻[ 𝑨 ] ⟶ 𝔻[ ⨅ ℬ ] h ⟨$⟩ a = λ i → ∣ 𝒽 i ∣ ⟨$⟩ a cong h xy i = cong ∣ 𝒽 i ∣ xy hhom : IsHom 𝑨 (⨅ ℬ) h compatible hhom = λ i → compatible ∥ 𝒽 i ∥
Two structures are isomorphic provided there are homomorphisms from each to the
other that compose to the identity. We define the following record type to
represent this concept. Note that the definition, shown below, includes a proof of
the fact that the maps to and from are bijective, which makes this fact more
accessible.
module _ (𝑨 : Algebra α ρᵃ) (𝑩 : Algebra β ρᵇ) where open Setoid 𝔻[ 𝑨 ] using () renaming ( _≈_ to _≈ᴬ_ ) open Setoid 𝔻[ 𝑩 ] using () renaming ( _≈_ to _≈ᴮ_ ) record _≅_ : Type (𝓞 ⊔ 𝓥 ⊔ α ⊔ ρᵃ ⊔ β ⊔ ρᵇ ) where constructor mkiso field to : hom 𝑨 𝑩 from : hom 𝑩 𝑨 to∼from : ∀ b → ∣ to ∣ ⟨$⟩ (∣ from ∣ ⟨$⟩ b) ≈ᴮ b from∼to : ∀ a → ∣ from ∣ ⟨$⟩ (∣ to ∣ ⟨$⟩ a) ≈ᴬ a toIsInjective : IsInjective ∣ to ∣ toIsInjective {x}{y} xy = trans (sym (from∼to x)) (trans ξ (from∼to y)) where open Setoid 𝔻[ 𝑨 ] using ( sym ; trans ) ξ : ∣ from ∣ ⟨$⟩ (∣ to ∣ ⟨$⟩ x) ≈ᴬ ∣ from ∣ ⟨$⟩ (∣ to ∣ ⟨$⟩ y) ξ = cong ∣ from ∣ xy fromIsSurjective : IsSurjective ∣ from ∣ fromIsSurjective {x} = eq (∣ to ∣ ⟨$⟩ x) (sym (from∼to x)) where open Setoid 𝔻[ 𝑨 ] using ( sym ) open _≅_
It is easy to prove that \ar{\au{}≅\au{}} is an equivalence relation, as follows.
≅-refl : Reflexive (_≅_ {α}{ρᵃ}) ≅-refl {α}{ρᵃ}{𝑨} = mkiso 𝒾𝒹 𝒾𝒹 (λ b → refl) λ a → refl where open Setoid 𝔻[ 𝑨 ] using ( refl ) ≅-sym : Sym (_≅_{β}{ρᵇ}) (_≅_{α}{ρᵃ}) ≅-sym φ = mkiso (from φ) (to φ) (from∼to φ) (to∼from φ) ≅-trans : Trans (_≅_ {α}{ρᵃ}) (_≅_{β}{ρᵇ}) (_≅_{α}{ρᵃ}{γ}{ρᶜ}) ≅-trans {ρᶜ = ρᶜ}{𝑨}{𝑩}{𝑪} ab bc = mkiso f g τ ν where f : hom 𝑨 𝑪 ; g : hom 𝑪 𝑨 f = ∘-hom (to ab) (to bc) ; g = ∘-hom (from bc) (from ab) open Setoid 𝔻[ 𝑨 ] using ( _≈_ ; trans ) open Setoid 𝔻[ 𝑪 ] using () renaming ( _≈_ to _≈ᶜ_ ; trans to transᶜ ) τ : ∀ b → ∣ f ∣ ⟨$⟩ (∣ g ∣ ⟨$⟩ b) ≈ᶜ b τ b = transᶜ (cong ∣ to bc ∣ (to∼from ab (∣ from bc ∣ ⟨$⟩ b))) (to∼from bc b) ν : ∀ a → ∣ g ∣ ⟨$⟩ (∣ f ∣ ⟨$⟩ a) ≈ a ν a = trans (cong ∣ from ab ∣ (from∼to bc (∣ to ab ∣ ⟨$⟩ a))) (from∼to ab a)
We have found that a useful way to encode the concept of homomorphic image is to produce a witness, that is, a surjective hom. Thus we define the type of surjective homs and also record the fact that an algebra is its own homomorphic image via the identity hom.
ov : Level → Level -- shorthand for a common level transformation ov α = 𝓞 ⊔ 𝓥 ⊔ suc α _IsHomImageOf_ : (𝑩 : Algebra β ρᵇ)(𝑨 : Algebra α ρᵃ) → Type _ 𝑩 IsHomImageOf 𝑨 = Σ[ φ ∈ hom 𝑨 𝑩 ] IsSurjective ∣ φ ∣ IdHomImage : {𝑨 : Algebra α ρᵃ} → 𝑨 IsHomImageOf 𝑨 IdHomImage {α = α}{𝑨 = 𝑨} = 𝒾𝒹 , λ {y} → Image_∋_.eq y refl where open Setoid 𝔻[ 𝑨 ] using ( refl )
Another theorem in the agda-algebras library, called HomFactor, formalizes
the following factorization result: if g : hom 𝑨 𝑩, h : hom 𝑨 𝑪, h is
surjective, and ker h ⊆ ker g, then there exists φ : hom 𝑪 𝑩 such that g = φ
∘ h. A special case of this result that we use below is the fact that the setoid
function factorization we saw above lifts to factorization of homomorphisms.
Moreover, we associate a homomorphism h with its image—which is (the domain
of) a subalgebra of the codomain of h—using the function HomIm defined
below.8
module _ {𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ} where HomIm : (h : hom 𝑨 𝑩) → Algebra _ _ Domain (HomIm h) = Im ∣ h ∣ Interp (HomIm h) ⟨$⟩ (f , la) = (f ̂ 𝑨) la cong (Interp (HomIm h)) {x1 , x2} {.x1 , y2} (≡.refl , e) = begin ∣ h ∣ ⟨$⟩ (Interp 𝑨 ⟨$⟩ (x1 , x2)) ≈⟨ h-compatible ⟩ Interp 𝑩 ⟨$⟩ (x1 , λ x → ∣ h ∣ ⟨$⟩ x2 x) ≈⟨ cong (Interp 𝑩) (≡.refl , e) ⟩ Interp 𝑩 ⟨$⟩ (x1 , λ x → ∣ h ∣ ⟨$⟩ y2 x) ≈˘⟨ h-compatible ⟩ ∣ h ∣ ⟨$⟩ (Interp 𝑨 ⟨$⟩ (x1 , y2)) ∎ where open Setoid 𝔻[ 𝑩 ] ; open SetoidReasoning 𝔻[ 𝑩 ] open IsHom ∥ h ∥ renaming (compatible to h-compatible) toHomIm : (h : hom 𝑨 𝑩) → hom 𝑨 (HomIm h) toHomIm h = toIm ∣ h ∣ , mkhom (reflˢ 𝔻[ 𝑩 ]) fromHomIm : (h : hom 𝑨 𝑩) → hom (HomIm h) 𝑩 fromHomIm h = fromIm ∣ h ∣ , mkhom (IsHom.compatible ∥ h ∥)
The Lift-Alg operation neatly resolves the technical problem of universe
non-cumulativity because isomorphism classes of algebras are closed under
Lift-Alg.
module _ {𝑨 : Algebra α ρᵃ}{ℓ : Level} where Lift-≅ˡ : 𝑨 ≅ (Lift-Algˡ 𝑨 ℓ) Lift-≅ˡ = mkiso ToLiftˡ FromLiftˡ (ToFromLiftˡ{𝑨 = 𝑨}) (FromToLiftˡ{𝑨 = 𝑨}{ℓ}) Lift-≅ʳ : 𝑨 ≅ (Lift-Algʳ 𝑨 ℓ) Lift-≅ʳ = mkiso ToLiftʳ FromLiftʳ (ToFromLiftʳ{𝑨 = 𝑨}) (FromToLiftʳ{𝑨 = 𝑨}{ℓ}) Lift-≅ : {𝑨 : Algebra α ρᵃ}{ℓ ρ : Level} → 𝑨 ≅ (Lift-Alg 𝑨 ℓ ρ) Lift-≅ = ≅-trans Lift-≅ˡ Lift-≅ʳ
We say that 𝑨 is a subalgebra of 𝑩 and write 𝑨 ≤ 𝑩 just in case 𝑨 can be homomorphically
embedded in 𝑩; in other terms, 𝑨 ≤ 𝑩 iff there exists an injective hom from 𝑨 to 𝑩.
_≤_ : Algebra α ρᵃ → Algebra β ρᵇ → Type _ 𝑨 ≤ 𝑩 = Σ[ h ∈ hom 𝑨 𝑩 ] IsInjective ∣ h ∣
The subalgebra relation is reflexive, by the identity monomorphism (and transitive by composition of monomorphisms, hence, a preorder, though we won’t need this fact here).
≤-reflexive : {𝑨 : Algebra α ρᵃ} → 𝑨 ≤ 𝑨 ≤-reflexive = 𝒾𝒹 , id
We conclude this section with a definition that will be useful later; it simply converts a monomorphism into a proof of a subalgebra relationship.
mon→≤ : {𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ} → mon 𝑨 𝑩 → 𝑨 ≤ 𝑩 mon→≤ {𝑨 = 𝑨}{𝑩} x = mon→intohom 𝑨 𝑩 x
Fix a signature 𝑆 and let X denote an arbitrary nonempty collection of variable symbols. Such a collection is called a context. Assume the symbols in X are distinct from the operation symbols of 𝑆, that is X ∩ ∣ 𝑆 ∣ = ∅. A word in the language of 𝑆 is a finite sequence of members of X ∪ ∣ 𝑆 ∣. We denote the
concatenation of such sequences by simple juxtaposition. Let S₀ denote the set of nullary operation symbols of 𝑆. We define by induction on n the sets Tₙ of words over X ∪ ∣ 𝑆 ∣ as follows: T₀ := X ∪ S₀ and
Tₙ₊₁ := Tₙ ∪ 𝒯ₙ, where 𝒯ₙ is the collection of all f t such that f : ∣ 𝑆 ∣ and t : ∥ 𝑆 ∥ f → 𝑇ₙ.
(Recall, ∥ 𝑆 ∥ f is the arity of the operation symbol f.)
An 𝑆-term is a term in the language of 𝑆 and the collection of all 𝑆-terms in the context X is Term X := ⋃ₙ Tₙ.
In type theory, this translates to two cases: variable injection and applying an operation symbol to a tuple of terms. This represents each term as a tree with an operation symbol at each node and a variable symbol at
each leaf ℊ; hence the constructor names (ℊ for “generator” and node for “node”) in the following inductively defined type.
data Term (X : Type χ) : Type (ov χ) where ℊ : X → Term X node : (f : ∣ 𝑆 ∣)(t : ∥ 𝑆 ∥ f → Term X) → Term X
We enrich the Term type to a setoid of 𝑆-terms, which will ultimately be the domain of an algebra, called the term algebra in the signature 𝑆. For this we need an equivalence relation on terms.
module _ {X : Type χ } where data _≃_ : Term X → Term X → Type (ov χ) where rfl : {x y : X} → x ≡ y → (ℊ x) ≃ (ℊ y) gnl : ∀ {f}{s t : ∥ 𝑆 ∥ f → Term X} → (∀ i → (s i) ≃ (t i)) → (node f s) ≃ (node f t)
It is easy to show that _≃_ is an equivalence relation as follows.
≃-isRefl : Reflexive _≃_ ≃-isRefl {ℊ _} = rfl ≡.refl ≃-isRefl {node _ _} = gnl λ _ → ≃-isRefl ≃-isSym : Symmetric _≃_ ≃-isSym (rfl x) = rfl (≡.sym x) ≃-isSym (gnl x) = gnl λ i → ≃-isSym (x i) ≃-isTrans : Transitive _≃_ ≃-isTrans (rfl x) (rfl y) = rfl (≡.trans x y) ≃-isTrans (gnl x) (gnl y) = gnl λ i → ≃-isTrans (x i) (y i) ≃-isEquiv : IsEquivalence _≃_ ≃-isEquiv = record { refl = ≃-isRefl ; sym = ≃-isSym ; trans = ≃-isTrans }
For a given signature 𝑆 and context X, we define the algebra 𝑻 X, known as the term algebra in
𝑆 over X. The domain of 𝑻 X is Term X and, for each operation symbol f : ∣ 𝑆 ∣, we define
f ̂ 𝑻 X to be the operation which maps each tuple t : ∥ 𝑆 ∥ f → Term X of terms to the formal
term f t.
TermSetoid : (X : Type χ) → Setoid _ _ TermSetoid X = record { Carrier = Term X ; _≈_ = _≃_ ; isEquivalence = ≃-isEquiv } 𝑻 : (X : Type χ) → Algebra (ov χ) (ov χ) Algebra.Domain (𝑻 X) = TermSetoid X Algebra.Interp (𝑻 X) ⟨$⟩ (f , ts) = node f ts cong (Algebra.Interp (𝑻 X)) (≡.refl , ss≃ts) = gnl ss≃ts
Fix a signature 𝑆 and a context X. An environment for 𝑨 and X is a setoid whose carrier
is a mapping from the variable symbols X to the domain 𝕌[ 𝐴 ] and whose equivalence relation is
point-wise equality. Our formalization of this concept is the same as that of [@Abel:2021], which
Abel uses to formalize Birkhoff’s completeness theorem.
module Environment (𝑨 : Algebra α ℓ) where open Setoid 𝔻[ 𝑨 ] using ( _≈_ ; refl ; sym ; trans ) Env : Type χ → Setoid _ _ Env X = record { Carrier = X → 𝕌[ 𝑨 ] ; _≈_ = λ ρ τ → (x : X) → ρ x ≈ τ x ; isEquivalence = record { refl = λ _ → refl ; sym = λ h x → sym (h x) ; trans = λ g h x → trans (g x)(h x) }}
The interpretation of a term evaluated in a particular environment is defined as follows.
⟦_⟧ : {X : Type χ}(t : Term X) → (Env X) ⟶ 𝔻[ 𝑨 ] ⟦ ℊ x ⟧ ⟨$⟩ ρ = ρ x ⟦ node f args ⟧ ⟨$⟩ ρ = (Interp 𝑨) ⟨$⟩ (f , λ i → ⟦ args i ⟧ ⟨$⟩ ρ) cong ⟦ ℊ x ⟧ u≈v = u≈v x cong ⟦ node f args ⟧ x≈y = cong (Interp 𝑨)(≡.refl , λ i → cong ⟦ args i ⟧ x≈y )
Two terms are proclaimed equal if they are equal for all environments.
Equal : {X : Type χ}(s t : Term X) → Type _ Equal {X = X} s t = ∀ (ρ : Carrier (Env X)) → ⟦ s ⟧ ⟨$⟩ ρ ≈ ⟦ t ⟧ ⟨$⟩ ρ
Proof that Equal is an equivalence relation, and that the implication s ≃ t → Equal s t holds for all terms s and t, are also found in [@Abel:2021]. We reproduce them here to keep the presentation self-contained.
≃→Equal : {X : Type χ}(s t : Term X) → s ≃ t → Equal s t ≃→Equal .(ℊ _) .(ℊ _) (rfl ≡.refl) = λ _ → refl ≃→Equal (node _ s)(node _ t)(gnl x) = λ ρ → cong (Interp 𝑨)(≡.refl , λ i → ≃→Equal(s i)(t i)(x i)ρ ) EqualIsEquiv : {Γ : Type χ} → IsEquivalence (Equal {X = Γ}) reflᵉ EqualIsEquiv = λ _ → refl symᵉ EqualIsEquiv = λ x=y ρ → sym (x=y ρ) transᵉ EqualIsEquiv = λ ij jk ρ → trans (ij ρ) (jk ρ)
We need to formalize two more concepts involving terms.
The first (comm-hom-term) is the assertion that every term commutes with every homomorphism, and
the second (interp-prod) is the interpretation of a term in a product algebra.
module _ {X : Type χ}{𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ}(hh : hom 𝑨 𝑩) where open Environment 𝑨 using ( ⟦_⟧ ) open Environment 𝑩 using () renaming ( ⟦_⟧ to ⟦_⟧ᴮ ) open Setoid 𝔻[ 𝑩 ] using ( _≈_ ; refl ) private hfunc = ∣ hh ∣ ; h = _⟨$⟩_ hfunc comm-hom-term : (t : Term X) (a : X → 𝕌[ 𝑨 ]) → h (⟦ t ⟧ ⟨$⟩ a) ≈ ⟦ t ⟧ᴮ ⟨$⟩ (h ∘ a) comm-hom-term (ℊ x) a = refl comm-hom-term (node f t) a = begin h(⟦ node f t ⟧ ⟨$⟩ a) ≈⟨ compatible ∥ hh ∥ ⟩ (f ̂ 𝑩)(λ i → h(⟦ t i ⟧ ⟨$⟩ a)) ≈⟨ cong(Interp 𝑩)(≡.refl , λ i → comm-hom-term(t i) a) ⟩ ⟦ node f t ⟧ᴮ ⟨$⟩ (h ∘ a) ∎ where open SetoidReasoning 𝔻[ 𝑩 ] module _ {X : Type χ}{ι : Level} {I : Type ι} (𝒜 : I → Algebra α ρᵃ) where open Setoid 𝔻[ ⨅ 𝒜 ] using ( _≈_ ) open Environment using ( ⟦_⟧ ; ≃→Equal ) interp-prod : (p : Term X) → ∀ ρ → (⟦ ⨅ 𝒜 ⟧ p) ⟨$⟩ ρ ≈ λ i → (⟦ 𝒜 i ⟧ p) ⟨$⟩ λ x → (ρ x) i interp-prod (ℊ x) = λ ρ i → ≃→Equal (𝒜 i) (ℊ x) (ℊ x) ≃-isRefl λ _ → (ρ x) i interp-prod (node f t) = λ ρ → cong (Interp (⨅ 𝒜)) ( ≡.refl , λ j k → interp-prod (t j) ρ k )
An 𝑆-term equation (or 𝑆-term identity) is an ordered pair (p , q) of 𝑆-terms, also denoted by p ≈ q. They are often simply called equations or identities, especially when the signature 𝑆 is evident.
We define an equational theory (or algebraic theory) to be a pair T = (𝑆 , ℰ) consisting of a signature 𝑆 and a collection ℰ of 𝑆-term equations.9
We say that the algebra 𝑨 models the identity p ≈ q and we write 𝑨 ⊧ p ≈ q
if for all ρ : X → 𝔻[ 𝑨 ] we have ⟦ p ⟧ ⟨$⟩ ρ ≈ ⟦ q ⟧ ⟨$⟩ ρ.
In other words, when interpreted in the algebra 𝑨, the terms p and q are equal no matter what values are assigned to variable symbols occurring in p and q.
If 𝒦 is a class of algebras of a given signature, then we write 𝒦 ⊫ p ≈ q and say that 𝒦 models the identity p ≈ q provided 𝑨 ⊧ p ≈ q for every 𝑨 ∈ 𝒦.
module _ {X : Type χ} where _⊧_≈_ : Algebra α ρᵃ → Term X → Term X → Type _ 𝑨 ⊧ p ≈ q = Equal p q where open Environment 𝑨 _⊫_≈_ : Pred (Algebra α ρᵃ) ℓ → Term X → Term X → Type _ 𝒦 ⊫ p ≈ q = ∀ 𝑨 → 𝒦 𝑨 → 𝑨 ⊧ p ≈ q
We represent a set of term identities as a predicate over pairs of terms, say, ℰ : Pred(Term X × Term X), and we denote by 𝑨 ⊨ ℰ the assertion that 𝑨 models p ≈ q for all (p, q) ∈ ℰ.
_⊨_ : (𝑨 : Algebra α ρᵃ) → Pred(Term X × Term X)(ov χ) → Type _ 𝑨 ⊨ ℰ = ∀ {p q} → (p , q) ∈ ℰ → Equal p q where open Environment 𝑨
(The symbol ⊨ is a stretched version of the models symbol ⊧,
so Agda can distinguish between the two and parse expressions involving the types
_⊨_ and _⊧_≈_. In Emacs agda2-mode, the symbol ⊨ is produced by typing
\|=, while ⊧ is produced with \models.)
An important property of the binary relation ⊧ is algebraic invariance (i.e.,
invariance under isomorphism). We formalize this property as follows.
module _ {X : Type χ}{𝑨 : Algebra α ρᵃ}(𝑩 : Algebra β ρᵇ)(p q : Term X) where ⊧-I-invar : 𝑨 ⊧ p ≈ q → 𝑨 ≅ 𝑩 → 𝑩 ⊧ p ≈ q ⊧-I-invar Apq (mkiso fh gh f∼g g∼f) ρ = begin ⟦ p ⟧ ⟨$⟩ ρ ≈˘⟨ cong ⟦ p ⟧ (f∼g ∘ ρ) ⟩ ⟦ p ⟧ ⟨$⟩ (f ∘ (g ∘ ρ)) ≈˘⟨ comm-hom-term fh p (g ∘ ρ) ⟩ f(⟦ p ⟧ᴬ ⟨$⟩ (g ∘ ρ)) ≈⟨ cong ∣ fh ∣ (Apq (g ∘ ρ)) ⟩ f(⟦ q ⟧ᴬ ⟨$⟩ (g ∘ ρ)) ≈⟨ comm-hom-term fh q (g ∘ ρ) ⟩ ⟦ q ⟧ ⟨$⟩ (f ∘ (g ∘ ρ)) ≈⟨ cong ⟦ q ⟧ (f∼g ∘ ρ) ⟩ ⟦ q ⟧ ⟨$⟩ ρ ∎ where private f = _⟨$⟩_ ∣ fh ∣ ; g = _⟨$⟩_ ∣ gh ∣ open Environment 𝑨 using () renaming ( ⟦_⟧ to ⟦_⟧ᴬ ) open Environment 𝑩 using ( ⟦_⟧ ) ; open SetoidReasoning 𝔻[ 𝑩 ]
If 𝒦 is a class of 𝑆-algebras, the set of identities modeled by 𝒦, denoted Th 𝒦, is called the equational theory of 𝒦. If ℰ is a set of 𝑆-term identities,
the class of algebras modeling ℰ, denoted Mod ℰ, is called the equational class axiomatized by ℰ. We codify these notions in the next two definitions.
Th : {X : Type χ} → Pred (Algebra α ρᵃ) ℓ → Pred(Term X × Term X) _ Th 𝒦 = λ (p , q) → 𝒦 ⊫ p ≈ q Mod : {X : Type χ} → Pred(Term X × Term X) ℓ → Pred (Algebra α ρᵃ) _ Mod ℰ 𝑨 = ∀ {p q} → (p , q) ∈ ℰ → Equal p q where open Environment 𝑨
Fix a signature 𝑆, let 𝒦 be a class of 𝑆-algebras, and define
H 𝒦 := the class of all homomorphic images of members of 𝒦;S 𝒦 := the class of all subalgebras of members of 𝒦;P 𝒦 := the class of all products of members of 𝒦.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. We represent these three closure operators in type theory as follows.
module _ {α ρᵃ β ρᵇ : Level} where private a = α ⊔ ρᵃ H : ∀ ℓ → Pred(Algebra α ρᵃ) (a ⊔ ov ℓ) → Pred(Algebra β ρᵇ) _ H _ 𝒦 𝑩 = Σ[ 𝑨 ∈ Algebra α ρᵃ ] 𝑨 ∈ 𝒦 × 𝑩 IsHomImageOf 𝑨 S : ∀ ℓ → Pred(Algebra α ρᵃ) (a ⊔ ov ℓ) → Pred(Algebra β ρᵇ) _ S _ 𝒦 𝑩 = Σ[ 𝑨 ∈ Algebra α ρᵃ ] 𝑨 ∈ 𝒦 × 𝑩 ≤ 𝑨 P : ∀ ℓ ι → Pred(Algebra α ρᵃ) (a ⊔ ov ℓ) → Pred(Algebra β ρᵇ) _ P _ ι 𝒦 𝑩 = Σ[ I ∈ Type ι ] (Σ[ 𝒜 ∈ (I → Algebra α ρᵃ) ] (∀ i → 𝒜 i ∈ 𝒦) × (𝑩 ≅ ⨅ 𝒜))
Identities modeled by an algebra 𝑨 are also modeled by every homomorphic image of
𝑨 and by every subalgebra of 𝑨. These facts are formalized in Agda as follows.
module _ {X : Type χ}{𝑨 : Algebra α ρᵃ}{𝑩 : Algebra β ρᵇ}{p q : Term X} where ⊧-H-invar : 𝑨 ⊧ p ≈ q → 𝑩 IsHomImageOf 𝑨 → 𝑩 ⊧ p ≈ q ⊧-H-invar Apq (φh , φE) ρ = begin ⟦ p ⟧ ⟨$⟩ ρ ≈˘⟨ cong ⟦ p ⟧(λ _ → InvIsInverseʳ φE) ⟩ ⟦ p ⟧ ⟨$⟩ (φ ∘ φ⁻¹ ∘ ρ) ≈˘⟨ comm-hom-term φh p (φ⁻¹ ∘ ρ) ⟩ φ( ⟦ p ⟧ᴬ ⟨$⟩ ( φ⁻¹ ∘ ρ)) ≈⟨ cong ∣ φh ∣ (Apq (φ⁻¹ ∘ ρ)) ⟩ φ( ⟦ q ⟧ᴬ ⟨$⟩ ( φ⁻¹ ∘ ρ)) ≈⟨ comm-hom-term φh q (φ⁻¹ ∘ ρ) ⟩ ⟦ q ⟧ ⟨$⟩ (φ ∘ φ⁻¹ ∘ ρ) ≈⟨ cong ⟦ q ⟧(λ _ → InvIsInverseʳ φE) ⟩ ⟦ q ⟧ ⟨$⟩ ρ ∎ where φ⁻¹ : 𝕌[ 𝑩 ] → 𝕌[ 𝑨 ] φ⁻¹ = SurjInv ∣ φh ∣ φE private φ = (_⟨$⟩_ ∣ φh ∣) open Environment 𝑨 using () renaming ( ⟦_⟧ to ⟦_⟧ᴬ) open Environment 𝑩 using ( ⟦_⟧ ) ; open SetoidReasoning 𝔻[ 𝑩 ] ⊧-S-invar : 𝑨 ⊧ p ≈ q → 𝑩 ≤ 𝑨 → 𝑩 ⊧ p ≈ q ⊧-S-invar Apq B≤A b = ∥ B≤A ∥ ( begin h ( ⟦ p ⟧ ⟨$⟩ b) ≈⟨ comm-hom-term hh p b ⟩ ⟦ p ⟧ᴬ ⟨$⟩ (h ∘ b) ≈⟨ Apq (h ∘ b) ⟩ ⟦ q ⟧ᴬ ⟨$⟩ (h ∘ b) ≈˘⟨ comm-hom-term hh q b ⟩ h ( ⟦ q ⟧ ⟨$⟩ b) ∎ ) where open SetoidReasoning 𝔻[ 𝑨 ] open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) open Environment 𝑨 using () renaming ( ⟦_⟧ to ⟦_⟧ᴬ ) open Environment 𝑩 using ( ⟦_⟧ ) private hh = ∣ B≤A ∣ ; h = _⟨$⟩_ ∣ hh ∣
An identity satisfied by all algebras in an indexed collection is also satisfied by the product of algebras in the collection.
module _ {X : Type χ}{I : Type ℓ}(𝒜 : I → Algebra α ρᵃ){p q : Term X} where ⊧-P-invar : (∀ i → 𝒜 i ⊧ p ≈ q) → ⨅ 𝒜 ⊧ p ≈ q ⊧-P-invar 𝒜pq a = begin ⟦ p ⟧₁ ⟨$⟩ a ≈⟨ interp-prod 𝒜 p a ⟩ ( λ i → (⟦ 𝒜 i ⟧ p) ⟨$⟩ λ x → (a x) i ) ≈⟨ (λ i → 𝒜pq i (λ x → (a x) i)) ⟩ ( λ i → (⟦ 𝒜 i ⟧ q) ⟨$⟩ λ x → (a x) i ) ≈˘⟨ interp-prod 𝒜 q a ⟩ ⟦ q ⟧₁ ⟨$⟩ a ∎ where open Environment (⨅ 𝒜) using () renaming ( ⟦_⟧ to ⟦_⟧₁ ) open Environment using ( ⟦_⟧ ) open Setoid 𝔻[ ⨅ 𝒜 ] using ( _≈_ ) open SetoidReasoning 𝔻[ ⨅ 𝒜 ]
A variety is a class of 𝑆-algebras that is closed under the taking of homomorphic images, subalgebras, and arbitrary products. If we define V 𝒦 := H (S (P 𝒦)), then 𝒦 is a variety iff V 𝒦 ⊆ 𝒦.
(The converse inclusion holds by virtue of the fact that V is a composition of closure operators.)
The class V 𝒦 is called the varietal closure of 𝒦. Here is how we define V in type theory.
(The explicit universe level declarations that appear in the definition are needed for disambiguation.)
module _ {α ρᵃ β ρᵇ γ ρᶜ δ ρᵈ : Level} where private a = α ⊔ ρᵃ ; b = β ⊔ ρᵇ V : ∀ ℓ ι → Pred(Algebra α ρᵃ) (a ⊔ ov ℓ) → Pred(Algebra δ ρᵈ) _ V ℓ ι 𝒦 = H{γ}{ρᶜ}{δ}{ρᵈ} (a ⊔ b ⊔ ℓ ⊔ ι) (S{β}{ρᵇ} (a ⊔ ℓ ⊔ ι) (P ℓ ι 𝒦))
The classes H 𝒦, S 𝒦, P 𝒦, and V 𝒦 all satisfy the
same term identities. We will only use a subset of the inclusions needed to prove this
assertion. (The others are included in the Setoid.Varieties.Preservation module of the agda-algebras library.) First, the closure operator H preserves the identities modeled by the given class; this follows almost immediately from the invariance lemma ⊧-H-invar.
module _ {X : Type χ}{𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)}{p q : Term X} where H-id1 : 𝒦 ⊫ p ≈ q → H{β = α}{ρᵃ}ℓ 𝒦 ⊫ p ≈ q H-id1 σ 𝑩 (𝑨 , kA , BimgA) = ⊧-H-invar{p = p}{q} (σ 𝑨 kA) BimgA
The analogous preservation result for S is a consequence of the invariance lemma ⊧-S-invar; the converse, which we call S-id2, has an equally straightforward proof.
S-id1 : 𝒦 ⊫ p ≈ q → S{β = α}{ρᵃ}ℓ 𝒦 ⊫ p ≈ q S-id1 σ 𝑩 (𝑨 , kA , B≤A) = ⊧-S-invar{p = p}{q} (σ 𝑨 kA) B≤A S-id2 : S ℓ 𝒦 ⊫ p ≈ q → 𝒦 ⊫ p ≈ q S-id2 Spq 𝑨 kA = Spq 𝑨 (𝑨 , (kA , ≤-reflexive))
The agda-algebras library includes analogous pairs of implications for P, H, and V, called P-id1, P-id2, H-id1, etc. Here we only need the first implication in each case, so we omit the others.
P-id1 : ∀{ι} → 𝒦 ⊫ p ≈ q → P{β = α}{ρᵃ}ℓ ι 𝒦 ⊫ p ≈ q P-id1 σ 𝑨 (I , 𝒜 , kA , A≅⨅A) = ⊧-I-invar 𝑨 p q IH (≅-sym A≅⨅A) where IH : ⨅ 𝒜 ⊧ p ≈ q IH = ⊧-P-invar 𝒜 {p}{q} λ i → σ (𝒜 i) (kA i) module _ {X : Type χ}{ι : Level}(ℓ : Level){𝒦 : Pred(Algebra α ρᵃ)(α ⊔ ρᵃ ⊔ ov ℓ)}{p q : Term X} where private aℓι = α ⊔ ρᵃ ⊔ ℓ ⊔ ι V-id1 : 𝒦 ⊫ p ≈ q → V ℓ ι 𝒦 ⊫ p ≈ q V-id1 σ 𝑩 (𝑨 , (⨅A , p⨅A , A≤⨅A) , BimgA) = H-id1{ℓ = aℓι}{𝒦 = S aℓι (P {β = α}{ρᵃ}ℓ ι 𝒦)}{p = p}{q} spK⊧pq 𝑩 (𝑨 , (spA , BimgA)) where spA : 𝑨 ∈ S aℓι (P {β = α}{ρᵃ}ℓ ι 𝒦) spA = ⨅A , (p⨅A , A≤⨅A) spK⊧pq : S aℓι (P ℓ ι 𝒦) ⊫ p ≈ q spK⊧pq = S-id1{ℓ = aℓι}{p = p}{q} (P-id1{ℓ = ℓ} {𝒦 = 𝒦}{p = p}{q} σ)
The term algebra 𝑻 X is the absolutely free 𝑆-algebra over X.
That is, for every 𝑆-algebra 𝑨, the following hold.
X to 𝕌[ 𝑨 ] lifts to a homomorphism from 𝑻 X to 𝑨.free-lift
and its setoid analog free-lift-func, and then proving the latter is a homomorphism.
(For the proof of uniqueness, see the Setoid.Terms.Properties module of the agda-algebras library.)module _ {X : Type χ}{𝑨 : Algebra α ρᵃ}(h : X → 𝕌[ 𝑨 ]) where free-lift : 𝕌[ 𝑻 X ] → 𝕌[ 𝑨 ] free-lift (ℊ x) = h x free-lift (node f t) = (f ̂ 𝑨) λ i → free-lift (t i) free-lift-func : 𝔻[ 𝑻 X ] ⟶ 𝔻[ 𝑨 ] free-lift-func ⟨$⟩ x = free-lift x cong free-lift-func = flcong where open Setoid 𝔻[ 𝑨 ] using ( _≈_ ) renaming ( reflexive to reflexiveᴬ ) flcong : ∀ {s t} → s ≃ t → free-lift s ≈ free-lift t flcong (_≃_.rfl x) = reflexiveᴬ (≡.cong h x) flcong (_≃_.gnl x) = cong (Interp 𝑨) (≡.refl , λ i → flcong (x i)) lift-hom : hom (𝑻 X) 𝑨 lift-hom = free-lift-func , mkhom λ{_}{a} → cong (Interp 𝑨) (≡.refl , λ i → (cong free-lift-func){a i} ≃-isRefl)
It turns out that the interpretation of a term p in an environment η is the same
as the free lift of η evaluated at p. We apply this fact a number of times in the sequel.
module _ {X : Type χ} {𝑨 : Algebra α ρᵃ} where open Setoid 𝔻[ 𝑨 ] using ( _≈_ ; refl ) open Environment 𝑨 using ( ⟦_⟧ ) free-lift-interp : (η : X → 𝕌[ 𝑨 ])(p : Term X) → ⟦ p ⟧ ⟨$⟩ η ≈ (free-lift{𝑨 = 𝑨} η) p free-lift-interp η (ℊ x) = refl free-lift-interp η (node f t) = cong (Interp 𝑨) (≡.refl , (free-lift-interp η) ∘ t)
Given an arbitrary class 𝒦 of 𝑆-algebras, we cannot expect that 𝑻 X belongs to 𝒦.
Indeed, there may be no free algebra in 𝒦.
Nonetheless, it is always possible to construct an algebra that is free for 𝒦 and belongs to the class S (P 𝒦).
Such an algebra is called a relatively free algebra over X (relative to 𝒦).
There are several informal approaches to defining this algebra.
We now describe the approach on which our formal construction is based and then we present the formalization.
Let 𝔽[ X ] denote the relatively free algebra over X. We represent 𝔽[ X ] as the quotient 𝑻 X / ≈ where x ≈ y if and only if h x = h y for every homomorphism h from 𝑻 X into a member of 𝒦.
More precisely, if 𝑨 ∈ 𝒦 and h : hom (𝑻 X) 𝑨, then h factors as 𝑻 X → HomIm h → 𝑨 and 𝑻 X / ker h ≅ HomIm h ≤ 𝑨; that is, 𝑻 X / ker h is (isomorphic to) an algebra in S 𝒦. Letting
≈ := ⋂ \{θ ∈ Con(𝑻 X) ∣ 𝑻 X / θ ∈ S 𝒦\},
observe that 𝔽[ X ] := 𝑻 X / ≈ is a subdirect product of the algebras 𝑻 X / ker h
as h ranges over all homomorphisms from 𝑻 X to algebras in 𝒦. Thus, 𝔽[ X ] ∈ P (S 𝒦) ⊆ S (P 𝒦).
As we have seen, every map ρ : X → 𝕌[ 𝑨 ] extends uniquely to a homomorphism h : hom (𝑻 X) 𝑨 and h
factors through the natural projection 𝑻 X → 𝔽[ X ] (since ≈ ⊆ ker h) yielding a unique homomorphism from 𝔽[ X ] to 𝑨 extending ρ.
In Agda we construct 𝔽[ X ] as a homomorphic image of 𝑻 X in the following way.
First, given X we define 𝑪 as the product of pairs (𝑨, ρ) of
algebras 𝑨 ∈ 𝒦 along with environments ρ : X → 𝕌[ 𝑨 ].
To do so, we contrive an index type for the product; each index is a triple (𝑨, p, ρ) where 𝑨 is an algebra, p is proof of 𝑨 ∈ 𝒦, and ρ : X → 𝕌[ 𝑨 ] is an arbitrary environment.
module FreeAlgebra (𝒦 : Pred (Algebra α ρᵃ) ℓ) where private c = α ⊔ ρᵃ ; ι = ov c ⊔ ℓ ℑ : {χ : Level} → Type χ → Type (ι ⊔ χ) ℑ X = Σ[ 𝑨 ∈ Algebra α ρᵃ ] 𝑨 ∈ 𝒦 × (X → 𝕌[ 𝑨 ]) 𝑪 : {χ : Level} → Type χ → Algebra (ι ⊔ χ)(ι ⊔ χ) 𝑪 X = ⨅ {I = ℑ X} ∣_∣
We then define 𝔽[ X ] to be the image of a homomorphism from 𝑻 X to 𝑪 as follows.
homC : (X : Type χ) → hom (𝑻 X) (𝑪 X) homC X = ⨅-hom-co _ (λ i → lift-hom (snd ∥ i ∥)) 𝔽[_] : {χ : Level} → Type χ → Algebra (ov χ) (ι ⊔ χ) 𝔽[ X ] = HomIm (homC X)
Observe that if the identity p ≈ q holds in all 𝑨 ∈ 𝒦 (for all environments), then p ≈ q holds in 𝔽[ X ]; equivalently, the pair (p , q) belongs to the kernel of the natural homomorphism from 𝑻 X onto 𝔽[ X ]. This natural epimorphism from 𝑻 X onto 𝔽[ X ]
is defined as follows.
module FreeHom {𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)} where private c = α ⊔ ρᵃ ; ι = ov c ⊔ ℓ open FreeAlgebra 𝒦 using ( 𝔽[_] ; homC ) epiF[_] : (X : Type c) → epi (𝑻 X) 𝔽[ X ] epiF[ X ] = ∣ toHomIm (homC X) ∣ , record { isHom = ∥ toHomIm (homC X) ∥ ; isSurjective = toIm-surj ∣ homC X ∣ } homF[_] : (X : Type c) → hom (𝑻 X) 𝔽[ X ] homF[ X ] = IsEpi.HomReduct ∥ epiF[ X ] ∥
Before formalizing the HSP theorem in the next section, we need to prove the following important property of the relatively free algebra: For every algebra 𝑨, if 𝑨 ⊨ Th (V 𝒦),
then there exists an epimorphism from 𝔽[ A ] onto 𝑨, where A denotes the carrier of 𝑨.
module _ {𝑨 : Algebra (α ⊔ ρᵃ ⊔ ℓ)(α ⊔ ρᵃ ⊔ ℓ)}{𝒦 : Pred(Algebra α ρᵃ)(α ⊔ ρᵃ ⊔ ov ℓ)} where private c = α ⊔ ρᵃ ⊔ ℓ ; ι = ov c open FreeAlgebra 𝒦 using ( 𝔽[_] ; 𝑪 ) open Setoid 𝔻[ 𝑨 ] using ( refl ; sym ; trans ) renaming ( Carrier to A ; _≈_ to _≈ᴬ_ ) F-ModTh-epi : 𝑨 ∈ Mod (Th 𝒦) → epi 𝔽[ A ] 𝑨 F-ModTh-epi A∈ModThK = φ , isEpi where φ : 𝔻[ 𝔽[ A ] ] ⟶ 𝔻[ 𝑨 ] _⟨$⟩_ φ = free-lift{𝑨 = 𝑨} id cong φ {p} {q} pq = Goal where lift-pq : (p , q) ∈ Th 𝒦 lift-pq 𝑩 x ρ = begin ⟦ p ⟧ ⟨$⟩ ρ ≈⟨ free-lift-interp {𝑨 = 𝑩} ρ p ⟩ free-lift ρ p ≈⟨ pq (𝑩 , x , ρ) ⟩ free-lift ρ q ≈˘⟨ free-lift-interp{𝑨 = 𝑩} ρ q ⟩ ⟦ q ⟧ ⟨$⟩ ρ ∎ where open SetoidReasoning 𝔻[ 𝑩 ] ; open Environment 𝑩 using ( ⟦_⟧ ) Goal : free-lift id p ≈ᴬ free-lift id q Goal = begin free-lift id p ≈˘⟨ free-lift-interp {𝑨 = 𝑨} id p ⟩ ⟦ p ⟧ ⟨$⟩ id ≈⟨ A∈ModThK {p = p} {q} lift-pq id ⟩ ⟦ q ⟧ ⟨$⟩ id ≈⟨ free-lift-interp {𝑨 = 𝑨} id q ⟩ free-lift id q ∎ where open SetoidReasoning 𝔻[ 𝑨 ] ; open Environment 𝑨 using ( ⟦_⟧ ) isEpi : IsEpi 𝔽[ A ] 𝑨 φ isEpi = record { isHom = mkhom refl ; isSurjective = eq (ℊ _) refl } F-ModThV-epi : 𝑨 ∈ Mod (Th (V ℓ ι 𝒦)) → epi 𝔽[ A ] 𝑨 F-ModThV-epi A∈ModThVK = F-ModTh-epi λ {p}{q} → Goal {p}{q} where Goal : 𝑨 ∈ Mod (Th 𝒦) Goal {p}{q} x ρ = A∈ModThVK{p}{q} (V-id1 ℓ {p = p}{q} x) ρ
Actually, we will need the following lifted version of this result.
F-ModTh-epi-lift : 𝑨 ∈ Mod (Th (V ℓ ι 𝒦)) → epi 𝔽[ A ] (Lift-Alg 𝑨 ι ι) F-ModTh-epi-lift A∈ModThK = ∘-epi (F-ModThV-epi λ {p q} → A∈ModThK{p = p}{q} ) ToLift-epi
Let 𝒦 be a class of algebras and recall that 𝒦 is a variety provided
it is closed under homomorphisms, subalgebras and products; equivalently,
V 𝒦 ⊆ 𝒦.
(Observe that 𝒦 ⊆ V 𝒦 holds for all 𝒦 since V is a closure operator.)
We call 𝒦 an equational class if it is the class of all models of some set of identities.
Birkhoff’s variety theorem, also known as the HSP theorem, asserts that 𝒦 is an equational class if and only if it is a variety. In this section, we present the statement and proof of this theorem—first in a style similar to what one finds in textbooks (e.g., [@Bergman:2012 Theorem 4.41]), and then formally in the language of MLTT.
(⇒) Every equational class is a variety. Indeed, suppose 𝒦 is an equational class axiomatized by term identities ℰ; that is, 𝑨 ∈ 𝒦 iff 𝑨 ⊨ ℰ. Since the classes H 𝒦, S 𝒦, P 𝒦 and 𝒦 all satisfy the same set of equations, we have V 𝒦 ⊫ p ≈ q for all (p , q) ∈ ℰ, so V 𝒦 ⊆ 𝒦.
(⇐) Every variety is an equational class.10 Let 𝒦 be an arbitrary variety. We will describe a set of equations that axiomatizes 𝒦. A natural choice is to take Th 𝒦 and try to prove that 𝒦 = Mod (Th 𝒦). Clearly, 𝒦 ⊆ Mod (Th 𝒦). To prove the converse inclusion, let 𝑨 ∈ Mod (Th 𝒦). It suffices to find an algebra 𝑭 ∈ S (P 𝒦) such that 𝑨 is a homomorphic image of 𝑭, as this will show that 𝑨 ∈ H (S (P 𝒦)) = 𝒦.
Let X be such that there exists a surjective environment ρ : X → 𝕌[ 𝑨 ].11
By the lift-hom lemma, there is an epimorphism h : 𝑻 X → 𝕌[ 𝑨 ] that extends ρ. Put 𝔽[ X ] := 𝑻 X / ≈ and let g : 𝑻 X → 𝔽[ X ] be the natural epimorphism with kernel ≈. We claim ker g ⊆ ker h.
If the claim is true, then there is a map f : 𝔽[ X ] → 𝑨 such that f ∘ g = h, and since h
is surjective so is f. Therefore, 𝑨 ∈ 𝖧 (𝔽[ X ]) ⊆ Mod (Th 𝒦) completing the proof.
It remains to prove the claim ker g ⊆ ker h. Let u, v be terms and assume g u = g v. Since 𝑻 X is generated by X, there are terms p, q such that u = ⟦ 𝑻 X ⟧ p and v = ⟦ 𝑻 X ⟧ q.12
Therefore, ⟦ 𝔽[ X ] ⟧ p = g (⟦ 𝑻 X ⟧ p) = g u = g v = g (⟦ 𝑻 X ⟧ q) = ⟦ 𝔽[ X ]⟧ q,
so 𝒦 ⊫ p ≈ q; thus, (p , q) ∈ Th 𝒦. Since 𝑨 ∈ Mod (Th 𝒦), we obtain 𝑨 ⊧ p ≈ q, which implies
that h u = (⟦ 𝑨 ⟧ p) ⟨$⟩ ρ = (⟦ 𝑨 ⟧ q) ⟨$⟩ ρ = h v, as desired.
(⇒) Every equational class is a variety.
We need an arbitrary equational class, which we obtain by starting with an arbitrary collection ℰ of equations and then defining 𝒦 = Mod ℰ, the class axiomatized by ℰ. We prove that 𝒦 is a variety by showing that 𝒦 = V 𝒦. The inclusion 𝒦 ⊆ V 𝒦, which holds for all classes 𝒦, is called the expansive property of V.
module _ (𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)) where V-expa : 𝒦 ⊆ V ℓ (ov (α ⊔ ρᵃ ⊔ ℓ)) 𝒦 V-expa {x = 𝑨}kA = 𝑨 , (𝑨 , (⊤ , (λ _ → 𝑨), (λ _ → kA), Goal), ≤-reflexive), IdHomImage where open Setoid 𝔻[ 𝑨 ] using ( refl ) open Setoid 𝔻[ ⨅ (λ _ → 𝑨) ] using () renaming ( refl to refl⨅ ) to⨅ : 𝔻[ 𝑨 ] ⟶ 𝔻[ ⨅ (λ _ → 𝑨) ] to⨅ = record { f = λ x _ → x ; cong = λ xy _ → xy } from⨅ : 𝔻[ ⨅ (λ _ → 𝑨) ] ⟶ 𝔻[ 𝑨 ] from⨅ = record { f = λ x → x tt ; cong = λ xy → xy tt } Goal : 𝑨 ≅ ⨅ (λ x → 𝑨) Goal = mkiso (to⨅ , mkhom refl⨅) (from⨅ , mkhom refl) (λ _ _ → refl) (λ _ → refl)
Observe how 𝑨 is expressed as (isomorphic to) a product with just one factor (itself), that is, the product
⨅ (λ x → 𝑨) indexed over the one-element type ⊤.
For the inclusion V 𝒦 ⊆ 𝒦, recall lemma V-id1 which asserts that 𝒦 ⊫ p ≈ q implies
V ℓ ι 𝒦 ⊫ p ≈ q; whence, if 𝒦 is an equational class, then V 𝒦 ⊆ 𝒦, as we now confirm.
module _ {ℓ : Level}{X : Type ℓ}{ℰ : {Y : Type ℓ} → Pred (Term Y × Term Y) (ov ℓ)} where private 𝒦 = Mod{α = ℓ}{ℓ}{X} ℰ -- an arbitrary equational class EqCl⇒Var : V ℓ (ov ℓ) 𝒦 ⊆ 𝒦 EqCl⇒Var {𝑨} vA {p} {q} pℰq ρ = V-id1 ℓ {𝒦} {p} {q} (λ _ x τ → x pℰq τ) 𝑨 vA ρ
By V-expa and Eqcl⇒Var, every equational class is a variety.
(⇐) Every variety is an equational class.
To fix an arbitrary variety, start with an arbitrary class 𝒦 of 𝑆-algebras and take the varietal closure, V 𝒦. We prove that V 𝒦 is precisely the collection of algebras that model Th (V 𝒦); that is, V 𝒦 = Mod (Th (V 𝒦)). The inclusion V 𝒦 ⊆ Mod (Th (V 𝒦)) is a consequence of the fact that Mod Th is a closure operator.
module _ (𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)){X : Type (α ⊔ ρᵃ ⊔ ℓ)} where private c = α ⊔ ρᵃ ⊔ ℓ ; ι = ov c ModTh-closure : V{β = β}{ρᵇ}{γ}{ρᶜ}{δ}{ρᵈ} ℓ ι 𝒦 ⊆ Mod{X = X} (Th (V ℓ ι 𝒦)) ModTh-closure {x = 𝑨} vA {p} {q} x ρ = x 𝑨 vA ρ
Our proof of the inclusion Mod( Th( V 𝒦)) ⊆ V 𝒦 is carried out in two steps.
𝔽[ X ] ≤ 𝑪 X.Mod (Th (V 𝒦)) is a homomorphic image of 𝔽[ X ].From the first item we have 𝔽[ X ] ∈ S( P 𝒦)), since 𝑪 X is a product of algebras in 𝒦. From this and the second item will follow Mod (Th (V 𝒦)) ⊆ H (S (P 𝒦)) (= V 𝒦), as desired.
To prove 𝔽[ X ] ≤ 𝑪 X, we construct a homomorphism from 𝔽[ X ] to 𝑪 X and then show it is injective,
so 𝔽[ X ] is (isomorphic to) a subalgebra of 𝑪 X.
open FreeHom {ℓ = ℓ}{𝒦} open FreeAlgebra 𝒦 using (homC ; 𝔽[_] ; 𝑪 ) homFC : hom 𝔽[ X ] (𝑪 X) homFC = fromHomIm (homC X) monFC : mon 𝔽[ X ] (𝑪 X) monFC = ∣ homFC ∣ , record { isHom = ∥ homFC ∥ ; isInjective = λ {x}{y}→ fromIm-inj ∣ homC X ∣ {x}{y} } F≤C : 𝔽[ X ] ≤ 𝑪 X F≤C = mon→≤ monFC open FreeAlgebra 𝒦 using ( ℑ ) SPF : 𝔽[ X ] ∈ S ι (P ℓ ι 𝒦) SPF = 𝑪 X , ((ℑ X) , (∣_∣ , ((λ i → fst ∥ i ∥) , ≅-refl))) , F≤C
Next we prove that every algebra in Mod (Th (V 𝒦)) is a homomorphic image of 𝔽[ X ]. Indeed,
module _ {𝒦 : Pred(Algebra α ρᵃ) (α ⊔ ρᵃ ⊔ ov ℓ)} where private c = α ⊔ ρᵃ ⊔ ℓ ; ι = ov c Var⇒EqCl : ∀ 𝑨 → 𝑨 ∈ Mod (Th (V ℓ ι 𝒦)) → 𝑨 ∈ V ℓ ι 𝒦 Var⇒EqCl 𝑨 ModThA = 𝔽[ 𝕌[ 𝑨 ] ] , (SPF{ℓ = ℓ} 𝒦 , Aim) where open FreeAlgebra 𝒦 using ( 𝔽[_] ) epiFlA : epi 𝔽[ 𝕌[ 𝑨 ] ] (Lift-Alg 𝑨 ι ι) epiFlA = F-ModTh-epi-lift{ℓ = ℓ} λ {p q} → ModThA{p = p}{q} φ : Lift-Alg 𝑨 ι ι IsHomImageOf 𝔽[ 𝕌[ 𝑨 ] ] φ = epi→ontohom 𝔽[ 𝕌[ 𝑨 ] ] (Lift-Alg 𝑨 ι ι) epiFlA Aim : 𝑨 IsHomImageOf 𝔽[ 𝕌[ 𝑨 ] ] Aim = ∘-hom ∣ φ ∣(from Lift-≅), ∘-IsSurjective _ _ ∥ φ ∥(fromIsSurjective(Lift-≅{𝑨 = 𝑨}))
By ModTh-closure and Var⇒EqCl, we have V 𝒦 = Mod (Th (V 𝒦)) for every class 𝒦 of 𝑆-algebras.
Thus, every variety is an equational class.
This completes the formal proof of Birkhoff’s variety theorem. ∎
How do we differ from the classical, set-theoretic approach? Most noticeable is our avoidance of all size issues. By using universe levels and level polymorphism, we always make sure we are in a large enough universe. So we can easily talk about “all algebras such that…” because these are always taken from a bounded (but arbitrary) universe.
Our use of setoids introduces nothing new: all the equivalence relations we use were already present in the classical proofs. The only “new” material is that we have to prove that functions respect those equivalences.
Our first attempt to formalize Birkhoff’s theorem was not sufficiently careful in its handling of variable symbols X. Specifically, this type was unconstrained; it is meant to represent the informal notion of a “sufficiently large” collection of variable symbols. Consequently, we postulated surjections from X onto the domains of all algebras in the class under consideration. But then, given a signature 𝑺 and a one-element 𝑆-algebra 𝑨, by choosing X to be the empty type ⊥, our surjectivity postulate gives a map from ⊥ onto the singleton domain of 𝑨. (For details, see the Demos.ContraX module which constructs the counterexample in Agda.)
There have been a number of efforts to formalize parts of universal algebra in type theory besides ours. The Coq proof assistant, based on the Calculus of Inductive Constructions, was used by Capretta, in [@Capretta:1999], and Spitters and Van der Weegen, in [@Spitters:2011], to formalized the basics of universal algebra and some classical algebraic structures. In [@Gunther:2018] Gunther et al developed what seemed (prior to the library) the most extensive libraryof formalized universal algebra to date. Like , [@Gunther:2018] is based on dependent type theory, is programmed in , and goes beyond the basic isomorphism theorems to include some equational logic. Although their coverage is less extensive than that of , Gunther et al do treat multi-sorted algebras, whereas is currently limited to single-sorted structures.
As noted by Abel [@Abel:2021], Amato et al, in [@Amato:2021], have formalized multi-sorted algebras with finitary operators in UniMath. The restriction to finitary operations was due to limitations of the UniMath type theory, which does not have W-types nor user-defined inductive types. Abel also notes that Lynge and Spitters, in [@Lynge:2019], formalize multi-sorted algebras with finitary operators in Homotopy type theory ([@HoTT]) using Coq. HoTT’s higher inductive types enable them to define quotients as types, without the need for setoids. Lynge and Spitters prove three isomorphism theorems concerning subalgebras and quotient algebras, but do not formalize universal algebras nor varieties. Finally, in [@Abel:2021], Abel gives a new formal proof of the soundness and completeness theorem for multi-sorted algebraic structures.
An alternative formalization based on classical set-theory was achieved in [@birkhoff-in-mizar:1999]. ↩
See the [Birkhoff.lagda]{.sans-serif} file in the [ualib/ualib.gitlab.io]{.sans-serif} repository (15 Jan 2021 commit 71f1738) [@ualib_v1.0.0]. ↩
[src/Demos/HSP.lagda]{.sans-serif} in the agda-algebras repository: [github.com/ualib/agda-algebras]{.sans-serif}. ↩
the axiom asserting that two point-wise equal functions are equal ↩
All submodules of the module in the library are also fully constructive in this sense. ↩
The code in this paragraph was suggested by an anonymous referee. ↩
suc ℓ denotes the successor of ℓ in the universe hierarchy. ↩
The definition of was provided by an anonymous referee; it is indeed simpler than trying to apply the general HomFactor theorem found in the agda-algebras library. ↩
Some authors reserve the term for a deductively closed set of equations, that is, a set of equations that is closed under entailment. ↩
The proof we present here is based on [@Bergman:2012 Theorem 4.41]. ↩
Informally, this is done by assuming X has cardinality at least max(| 𝕌[ 𝑨 ] |, ω). Later we will see how to construct an X with the required property in type theory. ↩
⟦ 𝑨 ⟧ t denotes the interpretation of the term t in the algebra 𝑨. ↩