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