#### Products of Setoid Algebras

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

{-# OPTIONS --without-K --exact-split --safe #-}

open import Base.Algebras.Basic using (𝓞 ; 𝓥 ; Signature)

module Setoid.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 Function.Base                          using ( flip )
open import Function.Bundles                       using ( Func )
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 ( f 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 Base.Overture.Preliminaries    using ( ∣_∣; ∥_∥)
open import Base.Overture.Surjective       using ( proj ; projIsOnto ) renaming ( IsSurjective to onto )
open import Setoid.Algebras.Basic {𝑆 = 𝑆}  using ( ⟦_⟧ ; Algebra ; _̂_ ; ov ; 𝕌[_])

private variable α ρ ι : Level

open Algebra

: {I : Type ι }(𝒜 : I  Algebra α ρ)  Algebra (α  ι) (ρ  ι)

Domain ( {I} 𝒜) =

record { Carrier =  i  Carrier (Domain (𝒜 i))

; _≈_ = λ a b   i  Domain (𝒜 i) ._≈_ (a i) (b i)

; isEquivalence =
record { refl  =     λ i  reflE  (isEqv (Domain (𝒜 i)))
; sym   =   λ x i  symE   (isEqv (Domain (𝒜 i)))(x i)
; trans = λ x y i  transE (isEqv (Domain (𝒜 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

module _ {𝒦 : Pred (Algebra α ρ) (ov α)} where

: Type (ov(α  ρ))
= Σ[ 𝑨  (Algebra α ρ) ] 𝑨  𝒦

𝔄 :   Algebra α ρ
𝔄 i =  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.

#### Proving the coordinate projections are surjective

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.

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