Agda UALib β

### Basic Definitions

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

```

#### The type of terms

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.

#### The term algebra

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 universal property

The term algebra `π» X` is absolutely free (or universal, or initial) for algebras in the signature `π`. That is, for every π-algebra `π¨`, the following hold.

1. Every function from `π` to `β£ π¨ β£` lifts to a homomorphism from `π» X` to `π¨`.
2. The homomorphism that exists by item 1 is unique.

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).