---
layout: default
title : "Setoid.Algebras.Products module (Agda Universal Algebra Library)"
date : "2021-07-03"
author: "agda-algebras development team"
---

#### Products of Setoid Algebras

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


<!--
```agda
{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Overture using (π“ž ; π“₯ ; Signature)

module Setoid.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 Function          using ( flip ; Func )
open import Level             using( _βŠ”_ ; Level )
open import Relation.Binary   using ( Setoid ;  IsEquivalence ; Decidable )
open import Relation.Binary.PropositionalEquality  using ( refl ; _≑_ )
open import Relation.Unary    using ( Pred ; _∈_ )

open Func           using ( cong ) renaming ( to to _⟨$⟩_ )
open Setoid         using ( Carrier ; _β‰ˆ_ ) renaming ( isEquivalence to isEqv )
open IsEquivalence  using () renaming ( refl to reflE ; sym to symE ; trans to transE )


-- Imports from agda-algebras -----------------------------------------------------
open import Overture  using ( proj₁; proj ; projIsOnto )
                      renaming ( IsSurjective to onto )

open import Setoid.Algebras.Basic {𝑆 = 𝑆}  using ( Algebra ; _^_ ; ov ; 𝔻[_] ; π•Œ[_])

private variable α ρ ι : Level

open Algebra
```
-->

```agda
β¨… : {I : Type ΞΉ }(π’œ : I β†’ Algebra Ξ± ρ) β†’ Algebra (Ξ± βŠ” ΞΉ) (ρ βŠ” ΞΉ)

Domain (β¨… {I} π’œ) =
  record  { Carrier = βˆ€ i β†’ π•Œ[ π’œ i ]
          ; _β‰ˆ_ = Ξ» a b β†’ βˆ€ i β†’ 𝔻[ π’œ i ] ._β‰ˆ_ (a i) (b i)
          ; isEquivalence =
             record  { refl   = Ξ» i      β†’ reflE   (isEqv 𝔻[ π’œ i ])
                     ; sym    = Ξ» x i    β†’ symE    (isEqv 𝔻[ π’œ i ])(x i)
                     ; trans  = Ξ» x y i  β†’ transE  (isEqv 𝔻[ π’œ i ])(x i)(y i)
                     }
          }

Interp (β¨… {I} π’œ) ⟨$⟩ (f , a) = Ξ» i β†’ (f ^ π’œ i) (flip a i)
cong (Interp (β¨… {I} π’œ)) (refl , f=g ) = Ξ» i β†’ cong  (Interp (π’œ i)) (refl , flip f=g i )
```


#### Products of classes of Algebras


```agda
module _ {𝒦 : Pred (Algebra Ξ± ρ) (ov Ξ±)} where

  β„‘ : Type (ov (Ξ± βŠ” ρ))
  β„‘ = Ξ£[ 𝑨 ∈ (Algebra Ξ± ρ) ] 𝑨 ∈ 𝒦

  𝔄 : β„‘ β†’ Algebra Ξ± ρ
  𝔄 i = (proj₁ i)

  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.

#### Surjectivity of coordinate projections

Suppose `I` is an index type and `π’œ : I β†’ Algebra Ξ± ρ` is an indexed collection of algebras.
Let `β¨… π’œ` be the product algebra defined above.  Given `i : I`, consider the projection of `β¨… π’œ`
onto the `i-th` coordinate.  Of course this projection ought to be a surjective map from `β¨… π’œ` onto
`π’œ i`.  However, this is impossible if `I` is just an arbitrary type.  Indeed, we must have an
equality defined on `I` and this equality must be decidable, and we must assume that
each factor of the product is nonempty.  In the [Setoid.Overture.Surjective][] module
we showed how to define a *decidable index type* in Agda. Here we use this to prove that the
projection of a product of algebras over such an index type is surjective.


```agda
module _  {I : Type ΞΉ}                  -- index type
           {_β‰Ÿ_ : Decidable{A = I} _≑_}  -- with decidable equality
           {π’œ : I β†’ Algebra Ξ± ρ}         -- indexed collection of algebras
           {π’œI : βˆ€ i β†’ π•Œ[ π’œ i ] }        -- each of which is nonempty
           where

  ProjAlgIsOnto : βˆ€{i} β†’ Ξ£[ h ∈ (π•Œ[ β¨… π’œ ] β†’ π•Œ[ π’œ i ]) ] onto h
  ProjAlgIsOnto {i} = (proj _β‰Ÿ_ π’œI i) , projIsOnto _β‰Ÿ_ π’œI
```