This section presents the Terms.Basic module of the Agda Universal Algebra Library.
The theoretical background that begins each subsection below is based on Cliff Bergmanβs textbook Bergman (2012), specifically, Section 4.3. Apart from notation, our presentation is similar to Bergmanβs, but we will be more concise, omitting some details and all examples, in order to more quickly arrive at our objective, which is to use type theory to express the concepts and formalize them in the Agda language. We refer the reader to Bergman (2012) for a more complete exposition of classical (informal) universal algebra.
{-# OPTIONS --without-K --exact-split --safe #-} open import Algebras.Signatures using (Signature; π; π₯) module Terms.Basic {π : Signature π π₯} where open import Homomorphisms.HomomorphicImages{π = π} public
Fix a signature π
and let X
denote an arbitrary nonempty collection of variable symbols. Assume the symbols in X
are distinct from the operation symbols of π
, that is X β© β£ π β£ = β
.
By a word in the language of π
, we mean a nonempty, 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 πβ
of words over X βͺ β£ π β£
as follows (cf. Bergman (2012) Def. 4.19):
πβ := X βͺ Sβ
and πβββ := πβ βͺ π―β
where π―β
is the collection of all π π‘
such that π : β£ π β£
and π‘ : β₯ π β₯ π β πβ
. (Recall, β₯ π β₯ π
is the arity of the operation symbol π.)
We define the collection of terms in the signature π
over X
by Term X := ββ πβ
. By an π-term we mean a term in the language of π
.
The definition of Term X
is recursive, indicating that an inductive type could be used to represent the semantic notion of terms in type theory. Indeed, such a representation is given by the following inductive type.
data Term {π§ : Universe}(X : π§ Μ ) : ov π§ Μ where generator : X β Term X node : (f : β£ π β£)(π‘ : β₯ π β₯ f β Term X) β Term X open Term
This is a very basic inductive type that represents each term as a tree with an operation symbol at each node
and a variable symbol at each leaf (generator
).
Notation. As usual, the type X
represents an arbitrary collection of variable symbols. Recall, ov π§ Μ
is our shorthand notation for the universe π β π₯ β π§ βΊ Μ
. Throughout this module the name of the first constructor of the Term
type will remain generator
. However, in all of the modules that follow this one, we will use the shorthand β
to denote the generator
constructor.
For a given signature π
, if the type Term X
is nonempty (equivalently, if X
or β£ π β£
is nonempty), then we can define an algebraic structure, denoted by π» X
and called the term algebra in the signature π
over X
. Terms are viewed as acting on other terms, so both the domain and basic operations of the algebra are the terms themselves.
For each operation symbol π : β£ π β£
, denote by π Μ (π» X)
the operation on Term X
which maps a tuple π‘ : β₯ π β₯ π β β£ π» X β£
to the formal term π π‘
.
Define π» X
to be the algebra with universe β£ π» X β£ := Term X
and operations π Μ (π» X)
, one for each symbol π
in β£ π β£
.
In Agda the term algebra can be defined as simply as one could hope.
π» : {π§ : Universe}(X : π§ Μ ) β Algebra (ov π§) π π» X = Term X , node
The term algebra π» X
is absolutely free (or universal, or initial) for algebras in the signature π
. That is, for every π-algebra π¨
, the following hold.
π
to β£ π¨ β£
lifts to a homomorphism from π» X
to π¨
.We now prove this in Agda, starting with the fact that every map from X
to β£ π¨ β£
lifts to a map from β£ π» X β£
to β£ π¨ β£
in a natural way, by induction on the structure of the given term.
module _ {π€ π§ : Universe}{X : π§ Μ } where free-lift : (π¨ : Algebra π€ π)(h : X β β£ π¨ β£) β β£ π» X β£ β β£ π¨ β£ free-lift _ h (generator x) = h x free-lift π¨ h (node f π‘) = (f Μ π¨) (Ξ» i β free-lift π¨ h (π‘ i))
Naturally, at the base step of the induction, when the term has the form generator
x, the free lift of h
agrees with h
. For the inductive step, when the
given term has the form node f π‘
, the free lift is defined as
follows: Assuming (the induction hypothesis) that we know the image of each
subterm π‘ i
under the free lift of h
, define the free lift at the
full term by applying f Μ π¨
to the images of the subterms.
The free lift so defined is a homomorphism by construction. Indeed, here is the trivial proof.
lift-hom : (π¨ : Algebra π€ π) β (X β β£ π¨ β£) β hom (π» X) π¨ lift-hom π¨ h = free-lift π¨ h , Ξ» f a β ap (f Μ π¨) refl
Finally, we prove that the homomorphism is unique. This requires funext π₯ π€
(i.e., function extensionality at universe levels π₯
and π€
) which we postulate by making it part of the premise in the following function type definition.
free-unique : funext π₯ π€ β (π¨ : Algebra π€ π)(g h : hom (π» X) π¨) β (β x β β£ g β£ (generator x) β‘ β£ h β£ (generator x)) ---------------------------------------------------- β β (t : Term X) β β£ g β£ t β‘ β£ h β£ t free-unique _ _ _ _ p (generator x) = p x free-unique fe π¨ g h p (node π π‘) = β£ g β£ (node π π‘) β‘β¨ β₯ g β₯ π π‘ β© (π Μ π¨)(β£ g β£ β π‘) β‘β¨ Ξ± β© (π Μ π¨)(β£ h β£ β π‘) β‘β¨ (β₯ h β₯ π π‘)β»ΒΉ β© β£ h β£ (node π π‘) β where Ξ± : (π Μ π¨) (β£ g β£ β π‘) β‘ (π Μ π¨) (β£ h β£ β π‘) Ξ± = ap (π Μ π¨) (fe Ξ» i β free-unique fe π¨ g h p (π‘ i))
Letβs account for what we have proved thus far about the term algebra. If we postulate a type X : π§ Μ
(representing an arbitrary collection of variable symbols) such that for each π
-algebra π¨
there is a map from X
to the domain of π¨
, then it follows that for every π
-algebra π¨
there is a homomorphism from π» X
to β£ π¨ β£
that βagrees with the original map on X
,β by which we mean that for all x : X
the lift evaluated at generator x
is equal to the original function evaluated at x
.
If we further assume that each of the mappings from X
to β£ π¨ β£
is surjective, then the homomorphisms constructed with free-lift
and lift-hom
are epimorphisms, as we now prove.
lift-of-epi-is-epi : {π¨ : Algebra π€ π}{hβ : X β β£ π¨ β£} --------------------------------- β Epic hβ β Epic β£ lift-hom π¨ hβ β£ lift-of-epi-is-epi {π¨}{hβ} hE y = Ξ³ where hββ»ΒΉy = Inv hβ (hE y) Ξ· : y β‘ β£ lift-hom π¨ hβ β£ (generator hββ»ΒΉy) Ξ· = (InvIsInv hβ (hE y))β»ΒΉ Ξ³ : Image β£ lift-hom π¨ hβ β£ β y Ξ³ = eq y (generator hββ»ΒΉy) Ξ·
The lift-hom
and lift-of-epi-is-epi
types will be called to action when such epimorphisms are needed later (e.g., in the Varieties module).