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

{-# OPTIONS --without-K --exact-split --safe #-} open import Algebras.Basic using ( π ; π₯ ; Signature ) module Algebras.Products {π : Signature π π₯} where -- Imports from Agda and the Agda Standard Library ------------------------------ open import Agda.Primitive using ( lsuc ; _β_ ; Level ) renaming ( Set to Type ) open import Data.Product using ( _,_ ; Ξ£ ; Ξ£-syntax ) open import Relation.Unary using ( Pred ; _β_ ; _β_ ) -- Imports from agda-algebras --------------------------------------------------- open import Overture.Preliminaries using (_β»ΒΉ; ππ; β£_β£; β₯_β₯) open import 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

(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 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 Ξ± = π β π₯ β lsuc Ξ±

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.