---
layout: default
title : "Setoid.Algebras.Basic module (Agda Universal Algebra Library)"
date : "2021-04-23"
author: "agda-algebras development team"
---

#### Basic definitions

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

An **algebra over a signature** `𝑆`{.AgdaGeneralizable} is a setoid (i.e., a carrier
type together with an equivalence relation on it) equipped with an interpretation
of every operation symbol of `𝑆`{.AgdaGeneralizable} 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`{.AgdaRecord}, 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`{.AgdaFunction} below for where the cost reappears.

This module is the canonical entry point for the `Setoid/` tree.  It defines the
`Algebra`{.AgdaRecord} record, two smart constructors for building one from an
ordinary interpretation function, the operation-interpretation operator
`_^_`{.AgdaFunction}, 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:

+  [Setoid.Algebras.Products][]: indexed products;
+  [Setoid.Algebras.Finite][]: finite algebras;
+  [Setoid.Algebras.Reduct][]: reducts (to a smaller signature);
+  [Setoid.Congruences.Basic][]: congruences and the quotients they generate;
+  [Setoid.Homomorphisms.Basic][]: structure-preserving maps between algebras.

<!--
```agda
{-# 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`{.AgdaFunction} 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.

```agda
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`{.AgdaFunction}; the signatures of `H`, `S`, and `P` in
[Setoid.Varieties.Closure][] add the corresponding equality, class, and index
levels explicitly.

The `Term`{.AgdaDatatype} 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.

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

The `Algebra`{.AgdaRecord} 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.

```agda
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 `⟨_⟩`{.AgdaFunction} translates an ordinary signature into a
signature over a setoid domain, together with its companion
`EqArgs`{.AgdaFunction}; it is defined in the signature-generic module
[Setoid.Signatures][].[^2]

`𝔻[_]`{.AgdaFunction} 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.

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

`π•Œ[_]`{.AgdaFunction} 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 `𝑨`{.AgdaGeneralizable} and
carries no notion of equality of its elements.

```agda
-- 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]

```agda
-- 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.

```agda
_Μ‚_ : (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`{.AgdaRecord} by hand means supplying the
`Interp`{.AgdaField} field as a `Func`{.AgdaRecord} `(⟨ 𝑆 ⟩ Domain) Domain`, whose
congruence proof must take apart the `Ξ£`/`EqArgs`{.AgdaFunction} 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`{.AgdaFunction} 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`{.AgdaFunction}
assembles the `Algebra`{.AgdaRecord}, discharging the `{o , _} {.o , _} (refl , argsβ‰ˆ)`
match internally.

```agda
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β‚š`{.AgdaFunction} specialises `mkAlgebra`{.AgdaFunction} 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`.

```agda
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`{.AgdaFunction} 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 α ρ`.

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

`Level-of-Carrier`{.AgdaFunction} is the **universe level of the carrier of an algebra**.

```agda
-- 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Λ‘`{.AgdaFunction} 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.

```agda
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Κ³`{.AgdaFunction} 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.

```agda
  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`{.AgdaFunction} 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-β‰…`{.AgdaFunction} of
[Setoid.Homomorphisms.Isomorphisms][] is the isomorphism that makes the move
harmless.

```agda
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`{.AgdaField}
      clause matches it as `(o , args)`, which needs the pair constructor `_,_` in scope.
      We therefore re-export `_,_` and `Ξ£-syntax`{.AgdaFunction} 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.