Skip to content

Setoid.Algebras.Basic

Basic definitions

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

An algebra over a signature 𝑆 is a setoid (i.e., a carrier type together with an equivalence relation on it) equipped with an interpretation of every operation symbol of 𝑆 as a function on that carrier which respects the equivalence.

That last clause is the entire difference from the type-based development: on a setoid an operation is not a bare function but a Func, that is, a function bundled with a proof that it sends related arguments to related results. Carrying the proof inside the structure yields quotients: a quotient algebra is the same carrier under a coarser equivalence, so forming one needs neither quotient types nor an axiom. That matters here, because the library is --safe --cubical-compatible, where function extensionality is unavailable; see the discussion at mkAlgebra below for where the cost reappears.

This module is the canonical entry point for the Setoid/ tree. It defines the Algebra record, two smart constructors for building one from an ordinary interpretation function, the operation-interpretation operator _^_, and the universe-lifting operations that let algebras at different levels be compared and related.

Modules most closely related to this one are the following:

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

module Setoid.Algebras.Basic where

-- Imports from the Agda and the Agda Standard Library --------------------
open import Agda.Primitive   using ( _βŠ”_ ; lsuc ) renaming ( Set to Type )
open import Data.Product     using ( _,_ ; Ξ£-syntax ) public
open import Function         using ( _∘_ ; _βˆ˜β‚‚_ ; Func ; _$_ )
open import Level            using ( Level )
open import Relation.Binary  using ( Setoid )

open import Relation.Binary.PropositionalEquality as ≑ using ( _≑_ ; refl )

-- Imports from the Agda Universal Algebra Library ----------------------
open import Overture             using ( OperationSymbolsOf ; ArityOf ; π“ž ; π“₯ ; Signature ; 𝑆 )
open import Overture.Operations  using ( Op )
open import Setoid.Signatures    using ( ⟨_⟩ )

private variable α ρ ι : Level

ov abbreviates the recurring level join ov Ξ± = π“ž βŠ” π“₯ βŠ” lsuc Ξ±; it combines the levels of operation symbols and arities with the successor of a caller-supplied level. Abbreviating this join keeps many common level expressions readable.

ov : {π“ž π“₯ : Level}{𝑆 : Signature π“ž π“₯} β†’ Level β†’ Level
ov {π“ž = π“ž}{π“₯ = π“₯} Ξ± = π“ž βŠ” π“₯ βŠ” lsuc Ξ±

Other modules combine this shorthand with whatever carrier, equality, class, and index levels their definitions quantify over. For example, Setoid.Algebras.Products accepts 𝒦 : Pred (Algebra Ξ± ρ) (ov Ξ±) and places the type of pairs (𝑨 , 𝑨 ∈ 𝒦) at ov (Ξ± βŠ” ρ), which is also the carrier level of class-product; the signatures of H, S, and P in Setoid.Varieties.Closure add the corresponding equality, class, and index levels explicitly.

The Term type over X : Type Ο‡ is defined at Type (ov Ο‡) because the term construction needs the levels of the operation symbols and arities, plus one more level for the carrier of the term itself.1

Setoid Algebras

Here we define algebras over a setoid, instead of a mere type with no equivalence on it.

open Func renaming ( to to _⟨$⟩_ ; cong to β‰ˆcong )

The Algebra defines a setoid algebra, which is just like an ordinary algebra but we require that all of its basic operations respect the underlying setoid equality. The Func record packs a function (f, aka apply, aka _⟨$⟩_) with a proof (cong) that the function respects equality.

record Algebra {𝑆 : Signature π“ž π“₯} Ξ± ρ : Type (π“ž βŠ” π“₯ βŠ” lsuc (Ξ± βŠ” ρ)) where
  field
    Domain : Setoid α ρ
    Interp : Func (⟨ 𝑆 ⟩ Domain) Domain
    --      ^^^^^^^^^^^^^^^^^^^^^^^ is a record type with two fields:
    --       1. a function  f : Carrier (⟨ 𝑆 ⟩ Domain)  β†’ Carrier Domain
    --       2. a proof cong : f Preserves _β‰ˆβ‚_ ⟢ _β‰ˆβ‚‚_ (that f preserves the setoid equalities)

  open Setoid Domain using ( _β‰ˆ_ )
  -- Actually, we already have the following: (it's called "reflexive"; see Structures.IsEquivalence)
  β‰‘β†’β‰ˆ : βˆ€{x}{y} β†’ x ≑ y β†’ x β‰ˆ y
  β‰‘β†’β‰ˆ refl = Setoid.refl Domain

open Algebra

The operator ⟨_⟩ translates an ordinary signature into a signature over a setoid domain, together with its companion EqArgs; it is defined in the signature-generic module Setoid.Signatures.2

𝔻[_] is the domain of an algebra, which is the setoid underlying it. In other words, the domain is the carrier and equivalence of the algebra, taken together. It is the projection to reach for whenever the equality matters.

𝔻[_] : Algebra {𝑆 = 𝑆} Ξ± ρ β†’  Setoid Ξ± ρ
𝔻[ 𝑨 ] = Domain 𝑨

π•Œ[_] forgets one step further, to the bare carrier type. Mathematically it is the underlying-set functor from algebras to sets, minus the equality: π•Œ[ 𝑨 ] is inhabited by the elements of 𝑨 and carries no notion of equality of its elements.

-- Forgetful functor: returns the carrier of (the domain of) 𝑨, forgetting its structure.
π•Œ[_] : Algebra {𝑆 = 𝑆} Ξ± ρ β†’  Type Ξ±
π•Œ[ 𝑨 ] = Setoid.Carrier 𝔻[ 𝑨 ]

We use the ascii symbol ^ to define an infix function for operation-symbol interpretation in an algebra.3

-- Interpretation of an operation symbol in an algebra.
_^_ : (f : OperationSymbolsOf 𝑆)(𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ Op (ArityOf 𝑆 f) π•Œ[ 𝑨 ]
f ^ 𝑨 = Ξ» a β†’ (Interp 𝑨) ⟨$⟩ (f , a)

We previously used a unicode symbol for this purpose; the definition is preserved for backward compatibility, but its use is deprecated in favor of the ascii version above. See ADR-002 Β§7 for the rationale.

_Μ‚_ : (f : OperationSymbolsOf 𝑆)(𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ) β†’ Op (ArityOf 𝑆 f) π•Œ[ 𝑨 ]
f Μ‚ 𝑨 = Ξ» a β†’ (Interp 𝑨) ⟨$⟩ (f , a)
{-# WARNING_ON_USAGE _Μ‚_
"The combining-caret notation `_Μ‚_` is deprecated as of v3.0 and will be removed
in v3.1.  Use the ASCII `_^_` defined immediately above.  See ADR-002 Β§7."
#-}

Smart constructors for concrete algebras

Authoring a concrete Algebra by hand means supplying the Interp field as a Func (⟨ 𝑆 ⟩ Domain) Domain, whose congruence proof must take apart the Ξ£/EqArgs encoding of ⟨ 𝑆 ⟩: the clause β‰ˆcong {o , _} {.o , _} (refl , argsβ‰ˆ) = … recurs verbatim in every such algebra (it appears across Examples.Setoid.* and Classical.Bundles.*). The two builders below package that destructuring once.

A fully automatic congruence is not derivable at this layer, and deliberately so. Passing from the pointwise hypothesis βˆ€ i β†’ u i β‰ˆ v i to f o u β‰ˆ f o v is exactly an application of function extensionality, which the Setoid development avoids on principle and which is in any case unavailable under --safe --cubical-compatible.

So each constructor still requires a per-operation, pointwise congruence cong-f; it removes only the (refl , argsβ‰ˆ) boilerplate, never the mathematical content.

mkAlgebra is the general builder. Given a carrier setoid 𝐃, an interpretation f of each operation symbol, and a proof cong-f that every f o respects pointwise setoid equality of its argument tuple, mkAlgebra assembles the Algebra, discharging the {o , _} {.o , _} (refl , argsβ‰ˆ) match internally.

module _ (𝐷 : Setoid α ρ) where
  open Setoid 𝐷 using (_β‰ˆ_) renaming (Carrier to D)
  mkAlgebra :
    (f : (o : OperationSymbolsOf 𝑆) β†’ Op (ArityOf 𝑆 o) D)
    β†’ (βˆ€ o  β†’ {u v : ArityOf 𝑆 o β†’ D} β†’ (βˆ€ i β†’ u i β‰ˆ v i) β†’ f o u β‰ˆ f o v)
    β†’ Algebra {𝑆 = 𝑆} Ξ± ρ
  mkAlgebra f cong-f .Domain = 𝐷
  mkAlgebra f cong-f .Interp ⟨$⟩ (o , args) = f o args
  mkAlgebra f cong-f .Interp .β‰ˆcong {o , _} {.o , _} (refl , argsβ‰ˆ) = cong-f o argsβ‰ˆ

mkAlgebraβ‚š specialises mkAlgebra to a carrier whose equality is propositional _≑_. It takes a bare type A, builds Domain = ≑.setoid A (a Setoid Ξ± Ξ±, so the result is Algebra Ξ± Ξ±), and asks for cong-f in pointwise _≑_ form; e.g., ≑.congβ‚‚ for a binary operation, as in the β„•βˆΈ-magma of Examples.Setoid.FreeMagma.

mkAlgebraβ‚š : (A : Type Ξ±)
  (f : (o : OperationSymbolsOf 𝑆) β†’ Op (ArityOf 𝑆 o) A)
  β†’ (βˆ€ o β†’ {u v : ArityOf 𝑆 o β†’ A} β†’ (βˆ€ i β†’ u i ≑ v i) β†’ f o u ≑ f o v)
  β†’ Algebra {𝑆 = 𝑆} Ξ± Ξ±
mkAlgebraβ‚š A f cong-f = mkAlgebra (≑.setoid A) f cong-f

Sometimes a level has to be named that is only implicit in an algebra's type. Because Agda's universes are non-cumulative, an algebra cannot be silently reused at a larger level; the two projections below recover the levels so that a caller can state the lifting it needs.

Level-of-Alg is the level of the algebra type, π“ž βŠ” π“₯ βŠ” lsuc (Ξ± βŠ” ρ), which is one universe above both the carrier and the equality, since Algebra Ξ± ρ is a record containing a Setoid Ξ± ρ.

-- The universe level of an algebra
Level-of-Alg : {Ξ± ρ π“ž π“₯ : Level}{𝑆 : Signature π“ž π“₯} β†’ Algebra {𝑆 = 𝑆} Ξ± ρ β†’ Level
Level-of-Alg {Ξ± = Ξ±}{ρ}{π“ž}{π“₯} _ = π“ž βŠ” π“₯ βŠ” lsuc (Ξ± βŠ” ρ)

Level-of-Carrier is the universe level of the carrier of an algebra.

-- The universe level of the carrier of an algebra
Level-of-Carrier : {Ξ± ρ π“ž π“₯  : Level}{𝑆 : Signature π“ž π“₯} β†’ Algebra {𝑆 = 𝑆} Ξ± ρ β†’ Level
Level-of-Carrier {Ξ± = Ξ±} _ = Ξ±

Level lifting setoid algebra types

Agda's universes are non-cumulative: an inhabitant of Type Ξ± is not an inhabitant of Type (Ξ± βŠ” β„“), so two algebras built at different levels cannot simply be compared, and a theorem proved about Algebra Ξ± ρ does not automatically apply to Algebra (Ξ± βŠ” β„“) ρ.

This bites constantly in universal algebra, where the closure operators of Setoid.Varieties.Closure move between levels at every step. The remedy is to lift an algebra explicitly, and the reason the remedy costs nothing mathematically is that a lifted algebra is isomorphic to the original: Setoid.Homomorphisms.Isomorphisms proves Lift-β‰… : 𝑨 β‰… Lift-Alg 𝑨 β„“ ρ, so isomorphism classes are closed under lifting and every isomorphism-invariant property survives it.

An algebra carries two independent levels: the carrier's α and the equality's ρ; so there are two liftings, and they are kept separate.

Lift-AlgΛ‘ raises the carrier level, from Ξ± to Ξ± βŠ” β„“, leaving the equality where it is. The carrier becomes Lift β„“ π•Œ[ 𝑨 ] and two lifted elements are related exactly when the elements underneath them were, so the equivalence is transported unchanged.

module _ {𝑆 : Signature π“ž π“₯}(𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ)(β„“ : Level) where
  open Algebra 𝑨  using ()     renaming ( Domain to A )
  open Setoid A   using (sym ; trans )  renaming ( Carrier to ∣A∣ ; _β‰ˆ_ to _β‰ˆβ‚_ ; refl to refl₁ )
  open Level


  Lift-AlgΛ‘ : Algebra {𝑆 = 𝑆} (Ξ± βŠ” β„“) ρ
  Lift-AlgΛ‘ .Domain =
    record  { Carrier = Lift β„“ ∣A∣
            ; _β‰ˆ_ = Ξ» x y β†’ lower x β‰ˆβ‚ lower y
            ; isEquivalence = record  { refl = refl₁ ; sym = sym ; trans = trans }
            }
  Lift-AlgΛ‘ .Interp ⟨$⟩ (f , la) = lift $ (f ^ 𝑨) (lower ∘ la)
  Lift-AlgΛ‘ .Interp .β‰ˆcong (refl , la=lb) = β‰ˆcong (Interp 𝑨) (refl , la=lb)

Lift-AlgΚ³ raises the level of the equality, from ρ to ρ βŠ” β„“, and leaves the carrier alone. The relation becomes Lift β„“ βˆ˜β‚‚ _β‰ˆβ‚_, a proposition-level lift of the original, and the equivalence proofs are re-wrapped accordingly.

  Lift-AlgΚ³ : Algebra {𝑆 = 𝑆} Ξ± (ρ βŠ” β„“)
  Lift-AlgΚ³ .Domain =
    record  { Carrier = ∣A∣
            ; _β‰ˆ_ = (Lift β„“) βˆ˜β‚‚ _β‰ˆβ‚_
            ; isEquivalence = record  { refl = lift refl₁
                                      ; sym = lift ∘ sym ∘ lower
                                      ; trans = Ξ» x y β†’ lift $ trans (lower x) (lower y)
                                      }
            }
  Lift-AlgΚ³ .Interp ⟨$⟩ (f , la) = (f ^ 𝑨) la
  Lift-AlgΚ³ .Interp .β‰ˆcong (refl , la≑lb) = lift $ β‰ˆcong (Interp 𝑨) (≑.refl , (lower ∘ la≑lb))

Lift-Alg composes the two, raising both levels at once: given target increments β„“β‚€ and ℓ₁ it produces an algebra at (Ξ± βŠ” β„“β‚€, ρ βŠ” ℓ₁). It is the operation the closure operators use to bring a class and a candidate algebra to a common level; Lift-β‰… of Setoid.Homomorphisms.Isomorphisms is the isomorphism that makes the move harmless.

Lift-Alg : (𝑨 : Algebra {𝑆 = 𝑆} Ξ± ρ)(β„“β‚€ ℓ₁ : Level) β†’ Algebra {𝑆 = 𝑆} (Ξ± βŠ” β„“β‚€) (ρ βŠ” ℓ₁)
Lift-Alg 𝑨 β„“β‚€ = Lift-AlgΚ³ (Lift-AlgΛ‘ 𝑨 β„“β‚€)

  1. This is why the term construction is a relative monad rather than a monad; see Setoid.Terms.Monad. ↩

  2. Because the carrier of ⟨ 𝑆 ⟩ Domain is a Ξ£-type, an Interp clause matches it as (o , args), which needs the pair constructor _,_ in scope. We therefore re-export _,_ and Ξ£-syntax from this module (and hence from the Setoid.Algebras barrel), so that pattern-matching such a carrier needs no separate Data.Product import, and no longer trips the misleading "βˆ™-Op is not a constructor of the datatype … Ξ£" error, which points at the operation symbol rather than at the missing _,_. ↩

  3. The _^_ symbol is definitionally identical to _Μ‚_ and was introduced for grep-friendliness and to survive shell-pipeline tooling. New Classical/ code uses _^_ exclusively; existing Setoid/ code may continue to use _Μ‚_ until v3.1. See ADR-002 Β§7 for the rationale and per-tree policy. ↩