Skip to content

Setoid.Algebras.Products

Products of Setoid Algebras

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

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

β¨… : {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

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.

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