Legacy.Base.Algebras.Products

Products of Algebras and Product Algebras

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

{-# OPTIONS --cubical-compatible --exact-split --safe #-}

open import Overture using ( 𝓞 ; 𝓥 ; Signature )

module Legacy.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 Legacy.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.