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

{-# OPTIONS --without-K --exact-split --safe #-} open import Overture using ( π ; π₯ ; Signature ) module Base.Algebras.Products {π : 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 ) open import Level using ( Level ; _β_ ; suc ) open import Relation.Unary using ( Pred ; _β_ ; _β_ ) -- Imports from agda-algebras --------------------------------------------------- open import Overture using (_β»ΒΉ; ππ; β£_β£; β₯_β₯) open import Base.Algebras.Basic {π = π} using ( Algebra ; _Μ_ ; algebra ) private variable Ξ± Ξ² Ο π : Level

From now on, the modules of the
agda-algebras library will assume a
fixed signature `π : Signature π π₯`

.

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

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

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 agda-algebras library a *product
of* `π`

-*algebras* is represented by the following type.

β¨ : {I : Type π }(π : I β Algebra Ξ± π ) β Algebra (π β Ξ±) π β¨ {I = I} π = ( β (i : I) β β£ π i β£ ) , -- domain of the product algebra Ξ» π π i β (π Μ π i) Ξ» x β π x i -- basic operations of the product algebra

The type just defined is the one that will be used throughout the
agda-algebras library 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 : Type π }(π : I β algebra Ξ± π) β algebra (π β Ξ±) π β¨ ' {I} π = record { carrier = β i β carrier (π i) -- domain ; opsymbol = Ξ» π π i β (opsymbol (π i)) π Ξ» x β π x i } -- basic operations

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

, the type `Algebra Ξ± π`

has
type `Type(π β π₯ β lsuc Ξ±)`

. Such types occur so often in the
agda-algebras library that we define
the following shorthand for their universes.

ov : Level β Level ov Ξ± = π β π₯ β suc Ξ±

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 Ξ± π β Type Ξ²`

, 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 Ξ± π) β Type Ξ²`

) 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 `π¦`

.

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.

module _ {π¦ : Pred (Algebra Ξ± π)(ov Ξ±)} where β : Type (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.