This is the Algebras.Products module of the Agda Universal Algebra Library.

Notice that we begin this module by assuming a signature `π : Signature π π₯`

which is then present and available throughout the module.

{-# OPTIONS --without-K --exact-split --safe #-} open import Algebras.Signatures using (Signature; π; π₯) module Algebras.Products {π : Signature π π₯} where open import Algebras.Algebras hiding (π; π₯) public

From now on, the modules of the UALib will assume a fixed signature `π : Signature π π₯`

. Notice that we have to import the `Signature`

type from Algebras.Signatures before the `module`

line so that we may declare the signature `π`

as a parameter of the Algebras.Products module.

Recall the informal definition of a *product* of `π`

-algebras. Given a type `I : π Μ`

and a family `π : I β Algebra π€ π`

, the *product* `β¨
π`

is the algebra whose domain is the Cartesian product `Ξ π κ I , β£ π π β£`

of the domains of the algebras in `π`

, and whose operations are defined as follows: if `π`

is a `J`

-ary operation symbol and if `π : Ξ π κ I , J β π π`

is an `I`

-tuple of `J`

-tuples such that `π π`

is a `J`

-tuple of elements of `π π`

(for each `π`

), then `(π Μ β¨
π) π := (i : I) β (π Μ π i)(π i)`

.

In the UALib a *product of* π-*algebras* is represented by the following type.

module _ {π€ π : Universe}{I : π Μ } where β¨ : (π : I β Algebra π€ π ) β Algebra (π β π€) π β¨ π = (Ξ i κ I , β£ π i β£) , -- domain of the product algebra Ξ» π π i β (π Μ π i) Ξ» x β π x i -- basic operations of the product algebra

(Alternative acceptable notation for the domain of the product is `β i β β£ π i β£`

.)

The type just defined is the one that will be used throughout the UALib whenever the product of an indexed collection of algebras (of type `Algebra`

) is required. However, for the sake of completeness, here is how one could define a type representing the product of algebras inhabiting the record type `algebra`

.

open algebra β¨ ' : (π : I β algebra π€ π) β algebra (π β π€) π β¨ ' π = record { univ = β i β univ (π i) ; -- domain op = Ξ» π π i β (op (π i)) π Ξ» x β π x i } -- basic operations

**Notation**. Given a signature `π : Signature π π₯`

, the type `Algebra π€ π`

has type `π β π₯ β π€ βΊ Μ`

. Such types occur so often in the UALib that we define the following shorthand for their universes.

ov : Universe β Universe ov π€ = π β π₯ β π€ βΊ

An arbitrary class `π¦`

of algebras is represented as a predicate over the type `Algebra π€ π`

, for some universe level `π€`

and signature `π`

. That is, `π¦ : Pred (Algebra π€ π) π¦`

, for some type `π¦`

. Later we will formally state and prove that the product of all subalgebras of algebras in `π¦`

belongs to the class `SP(π¦)`

of subalgebras of products of algebras in `π¦`

. That is, `β¨
S(π¦) β SP(π¦ )`

. This turns out to be a nontrivial exercise.

To begin, we need to define types that represent products over arbitrary (nonindexed) families such as `π¦`

or `S(π¦)`

. Observe that `Ξ π¦`

is certainly not what we want. For recall that `Pred (Algebra π€ π) π¦`

is just an alias for the function type `Algebra π€ π β π¦ Μ`

, and the semantics of the latter takes `π¦ π¨`

(and `π¨ β π¦`

) to mean that `π¨`

belongs to the class `π¦`

. Thus, by definition,

`Ξ π¦ = Ξ π¨ κ (Algebra π€ π) , π¦ π¨`

Β Β `=`

Β Β `β (π¨ : Algebra π€ π) β π¨ β π¦`

,

which asserts that every inhabitant of the type `Algebra π€ π`

belongs to `π¦`

. Evidently this is not the product algebra that we seek.

What we need is a type that serves to index the class `π¦`

, and a function `π`

that maps an index to the inhabitant of `π¦`

at that index. But `π¦`

is a predicate (of type `(Algebra π€ π) β π¦ Μ`

) and the type `Algebra π€ π`

seems rather nebulous in that there is no natural indexing class with which to βenumerateβ all inhabitants of `Algebra π€ π`

belonging to `π¦`

.^{1}

The solution is to essentially take `π¦`

itself to be the indexing type, at least heuristically that is how one can view the type `β`

that we now define.^{2}

module class-products {π€ : Universe} (π¦ : Pred (Algebra π€ π)(ov π€)) where β : ov π€ Μ β = Ξ£ π¨ κ (Algebra π€ π) , (π¨ β π¦)

Taking the product over the index type `β`

requires a function that maps an index `i : β`

to the corresponding algebra. Each `i : β`

is a pair, `(π¨ , p)`

, where `π¨`

is an algebra and `p`

is a proof that `π¨`

belongs to `π¦`

, so the function mapping an index to the corresponding algebra is simply the first projection.

π : β β Algebra π€ π π i = β£ i β£

Finally, we define `class-product`

which represents the product of all members of π¦.

class-product : Algebra (ov π€) π class-product = β¨ π

If `p : π¨ β π¦`

, we view the pair `(π¨ , p) β β`

as an *index* over the class, so we can think of `π (π¨ , p)`

(which is simply `π¨`

) as the projection of the product `β¨
π`

onto the `(π¨ , p)`

-th component.

^{1} If you havenβt seen this before, give it some thought and see if the correct type comes to you organically.

^{2} **Unicode Hints**. Some of our types are denoted with with Gothic (βmathfrakβ) symbols. To produce them in agda2-mode, type `\Mf`

followed by a letter. For example, `\MfI`

β `β`

.