This is the Base.Algebras.Products module of the Agda Universal Algebra Library.
{-# OPTIONS --without-K --exact-split --safe #-} open import Overture using ( π ; π₯ ; Signature ) module 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 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 Ξ±
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.