Skip to content

Setoid.Algebras.Basic

Basic definitions

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

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

open import Overture using (π“ž ; π“₯ ; Signature )

module Setoid.Algebras.Basic {𝑆 : Signature π“ž π“₯} 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 )
open import Overture.Operations  using ( Op )
open import Setoid.Signatures    using ( ⟨_⟩ )

private variable α ρ ι : Level

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

Setoid Algebras

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

The operator ⟨_⟩ that translates an ordinary signature into a signature over a setoid domain β€” together with its companion EqArgs β€” is defined in the signature-generic module Setoid.Signatures and imported here (see the import above). Each takes its own signature argument rather than reading this module's {𝑆}, so housing them in a non-parameterized module means the unused {𝑆 : Signature π“ž π“₯} parameter of this module does not ride along as an unsolvable metavariable at use sites. The Interp field of Algebra applies the imported ⟨ 𝑆 ⟩ to this module's signature 𝑆.

Because the carrier of ⟨ 𝑆 ⟩ Domain is a Ξ£-type β€” an operation symbol paired with its argument tuple β€” 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 _,_.

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

A setoid algebra is just like an algebra but we require that all basic operations of the algebra 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 Ξ± ρ : 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 next three definitions are merely syntactic sugar that we sometimes use to make the code more readable.

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

-- 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.1

-- 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 we want to extract the universe level of a given algebra or its carrier. The following functions provide that information.

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

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

Level lifting setoid algebra types

module _ (𝑨 : 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Κ³ : 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 : (𝑨 : Algebra Ξ± ρ)(β„“β‚€ ℓ₁ : Level) β†’ Algebra (Ξ± βŠ” β„“β‚€) (ρ βŠ” ℓ₁)
Lift-Alg 𝑨 β„“β‚€ = Lift-AlgΚ³ (Lift-AlgΛ‘ 𝑨 β„“β‚€)

  1. 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. ↩