---
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][].

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

```agda
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 `⟨_⟩`{.AgdaFunction} that translates an ordinary signature into a
signature over a setoid domain β€” together with its companion `EqArgs`{.AgdaFunction}
β€” 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`{.AgdaField} field of
`Algebra`{.AgdaRecord} 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`{.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 `_,_`.

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

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

```agda
𝔻[_] : 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]

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

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

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