↑ Top

---

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 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 ( ∣_∣; ∥_∥ )
open import Base.Functions  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.

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.

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

---

← Setoid.Algebras.Basic Setoid.Algebras.Congruences →