### Products of Algebras and Product Algebras

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 Ξ±
```

### Products of classes of algebras

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.