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

### <a id="basic-definitions">Basic definitions</a>

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


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

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

module Legacy.Base.Algebras.Basic {𝑆 : Signature π“ž π“₯ } where

open import Agda.Primitive using () renaming ( Set to  Type )

-- Imports from the Agda Standard Library -------------------------------------
open import Data.Product     using ( _,_ ; _Γ—_ ; Ξ£-syntax )
open import Level            using ( Level ; _βŠ”_ ; suc )
open import Relation.Binary  using ( IsEquivalence ) renaming ( Rel to BinRel )
open import Relation.Unary   using ( _∈_ ; Pred )


-- Imports from the Agda Universal Algebra Library ----------------------------
open  import Overture        using ( ∣_∣ ; βˆ₯_βˆ₯ ; Op )
open  import Legacy.Base.Relations  using ( _|:_ ; _|:pred_ ; Rel ; compatible-Rel )
                             using ( REL ; compatible-REL )

private variable α β ρ : Level
```


#### <a id="algebras">Algebras</a>

Our first goal is to develop a working vocabulary and formal library for classical
(single-sorted, set-based) universal algebra.  In this section we define the main
objects of study.  An *algebraic structure* (or *algebra*) in the signature
`𝑆 = (𝐹, ρ)` is denoted by `𝑨 = (A, Fᴬ)` and consists of

*  `A` := a *nonempty* set (or type), called the *domain* (or *carrier* or
   *universe*) of the algebra;
*  `Fᴬ := { fᴬ ∣ f ∈ F, : (ρf β†’ A) β†’ A }`, a collection of *operations* on `𝑨`;
*  a (potentially empty) collection of *identities* satisfied by elements and
   *operations of `𝑨`.

Note that to each operation symbol `f ∈ 𝐹` corresponds an operation
`fᴬ` on `𝑨` of arity `ρf`; we call such `fᴬ` the *interpretation* of the symbol
`f` in the algebra `𝑨`. We call an algebra in the signature `𝑆` an `𝑆`-*algebra*.
An algebra is called *finite* if it has a finite domain, and is called *trivial*
if its universe is a singleton.  Given two algebras `𝑨` and `𝑩`, we say that `𝑩`
is a *reduct* of `𝑨` if both algebras have the same domain and `𝑩` can be obtained
from `𝑨` by simply removing some of the operations.

Recall, we defined the type `Signature π“ž π“₯` above as the dependent pair type
`Ξ£ F κž‰ Type π“ž , (F β†’ Type π“₯)`, and the type `Op` of operation symbols is the
function type `Op I A = (I β†’ A) β†’ A` (see [Legacy.Base.Relations.Discrete][]).

For a fixed signature `𝑆 : Signature π“ž π“₯` and universe level `Ξ±`, we define the
*type of algebras in the signature* `𝑆` (or *type of* `𝑆`-*algebras*) *with domain
type* `Type Ξ±` as follows.

```agda
Algebra : (Ξ± : Level) β†’ Type (π“ž βŠ” π“₯ βŠ” suc Ξ±)
Algebra α =  Σ[ A ∈ Type α ]                 -- the domain
             βˆ€ (f : ∣ 𝑆 ∣) β†’ Op (βˆ₯ 𝑆 βˆ₯ f) A  -- the basic operations
```

It would be more precise to refer to inhabitants of this type as ∞-*algebras*
because their domains can be of arbitrary type and need not be truncated at some
level and, in particular, need to be a set. (See [Legacy.Base.Equality.Truncation][].)

We might take this opportunity to define the type of 0-*algebras*, that is,
algebras whose domains are sets, which is probably closer to what most of us think
of when doing informal universal algebra.  However, in the
[agda-algebras](https://github.com/ualib/agda-algebras) library we will only need
to know that the domains of certain algebras are sets in a few places, so it seems
preferable to work with general (∞-)algebras throughout and then explicitly
postulate additional axioms (e.g., [uniquness of identity
proofs](https://ualib.github.io/agda-algebras/Equality.Truncation.html#uniqueness-of-identity-proofs)
if and only if necessary.


#### <a id="algebras-as-record-types">Algebras as record types</a>

A popular way to represent algebraic structures in type theory is with record
types.  The Sigma type defined above provides an equivalent alternative that we
happen to prefer and we use it throughout the library, both for consistency and
because of its direct connection to the existential quantifier of logic. Recall
that the type `Ξ£ x κž‰ X , P x` represents the proposition, "there exists `x` in `X`
such that `P x` holds;" in symbols, `βˆƒ x ∈ X , P x`.  Indeed, an inhabitant of `Ξ£
x κž‰ X , P x` is a pair `(x , p)` such that `x` inhabits `X` and `p` is a proof of
`P x`. In other terms, the pair `(x , p)` is a witness and proof of the
proposition `βˆƒ x ∈ X , P x`.

Nonetheless, for those who prefer to represent algebraic structures in type theory
using records, we offer the following definition (which is equivalent to the Sigma
type formulation).

```agda
record algebra (Ξ± : Level) : Type(suc(π“ž βŠ” π“₯ βŠ” Ξ±)) where
 constructor mkalg
 field
  carrier : Type Ξ±
  opsymbol : (f : ∣ 𝑆 ∣) β†’ ((βˆ₯ 𝑆 βˆ₯ f) β†’ carrier) β†’ carrier
```

This representation of algebras as inhabitants of a record type is equivalent to
the representation using Sigma types in the sense that a bi-implication between
the two representations is obvious.


```agda
open algebra

algebra→Algebra : algebra α → Algebra α
algebraβ†’Algebra 𝑨 = (carrier 𝑨 , opsymbol 𝑨)

Algebra→algebra : Algebra α → algebra α
Algebraβ†’algebra 𝑨 = mkalg ∣ 𝑨 ∣ βˆ₯ 𝑨 βˆ₯
```


#### <a id="operation-interpretation-syntax">Operation interpretation syntax</a>

We now define a convenient shorthand for the interpretation of an operation symbol.
This looks more similar to the standard notation one finds in the literature as
compared to the double bar notation we started with, so we will use this new notation
almost exclusively in the remaining modules of the [agda-algebras][] library.


```agda
_Μ‚_ : (𝑓 : ∣ 𝑆 ∣)(𝑨 : Algebra Ξ±) β†’ (βˆ₯ 𝑆 βˆ₯ 𝑓  β†’  ∣ 𝑨 ∣) β†’ ∣ 𝑨 ∣
𝑓 Μ‚ 𝑨 = Ξ» π‘Ž β†’ (βˆ₯ 𝑨 βˆ₯ 𝑓) π‘Ž
```

So, if `𝑓 : ∣ 𝑆 ∣` is an operation symbol in the signature `𝑆`, and if
`π‘Ž : βˆ₯ 𝑆 βˆ₯ 𝑓 β†’ ∣ 𝑨 ∣` is a tuple of the appropriate arity, then `(𝑓 Μ‚ 𝑨) π‘Ž`
denotes the operation `𝑓` interpreted in `𝑨` and evaluated at `π‘Ž`.

#### <a id="the-universe-level-of-an-algebra">The universe level of an algebra</a>

Occasionally we will be given an algebra and we just need to know the universe
level of its domain. The following utility function provides this.

```agda
Level-of-Alg : {Ξ± : Level} β†’ Algebra Ξ± β†’ Level
Level-of-Alg {Ξ± = Ξ±} _ = π“ž βŠ” π“₯ βŠ” suc Ξ±

Level-of-Carrier : {Ξ±  : Level} β†’ Algebra Ξ± β†’ Level
Level-of-Carrier {Ξ± = Ξ±} _ = Ξ±
```


#### <a id="lifts-of-algebras">Level lifting algebra types</a>

Recall, in the [section on level lifting and
lowering](/Functions/Lifts/#level-lifting-and-lowering), we described the
difficulties one may encounter when working with a noncumulative universe
hierarchy. We made a promise to provide some domain-specific level lifting and
level lowering methods. Here we fulfill this promise by supplying a couple of
bespoke tools designed specifically for our operation and algebra types.


```agda
open Level

Lift-alg-op : {I : Type π“₯} {A : Type Ξ±} β†’ Op I A β†’ (Ξ² : Level) β†’ Op I (Lift Ξ² A)
Lift-alg-op f Ξ² = Ξ» x β†’ lift (f (Ξ» i β†’ lower (x i)))

Lift-Alg : Algebra Ξ± β†’ (Ξ² : Level) β†’ Algebra (Ξ± βŠ” Ξ²)
Lift-Alg 𝑨 Ξ² = Lift Ξ² ∣ 𝑨 ∣ , (Ξ» (𝑓 : ∣ 𝑆 ∣) β†’ Lift-alg-op (𝑓 Μ‚ 𝑨) Ξ²)

open algebra

Lift-algebra : algebra Ξ± β†’ (Ξ² : Level) β†’ algebra (Ξ± βŠ” Ξ²)
Lift-algebra  𝑨 Ξ² =  mkalg (Lift Ξ² (carrier 𝑨)) (Ξ» (f : ∣ 𝑆 ∣)
 β†’                   Lift-alg-op ((opsymbol 𝑨) f) Ξ²)
```

What makes the `Lift-Alg` type so useful for resolving type level errors involving
algebras is the nice properties it possesses.  Indeed, the [agda-algebras][]
library contains formal proofs of the following facts.

+  [`Lift-Alg` is a homomorphism](/Legacy/Base/Homomorphisms/Basic/#exmples-of-homomorphisms)
   (see [Legacy.Base.Homomorphisms.Basic][])
+  [`Lift-Alg` is an algebraic invariant](/Legacy/Base/Homomorphisms/Isomorphisms/#lift-is-an-algebraic-invariant)
   (see [Legacy.Base.Homomorphisms.Isomorphisms][])
+  [`Lift-Alg` of a subalgebra is a subalgebra](/Legacy/Base/Subalgebras/Subalgebras/#lifts-of-subalgebras)
   (see [Legacy.Base.Subalgebras.Subalgebras][])
+  [`Lift-Alg` preserves identities](/Legacy/Base/Varieties/EquationalLogic/#lift-invariance))
  (see [Legacy.Base.Varieties.EquationalLogic][])


#### <a id="compatibility-of-binary-relations">Compatibility of binary relations</a>

We now define the function `compatible` so that, if `𝑨` denotes an algebra and `R`
a binary relation, then `compatible 𝑨 R` will represent the assertion that `R` is
*compatible* with all basic operations of `𝑨`. The formal definition is immediate
since all the work is done by the relation `|:`, which we defined above (see
[Legacy.Base.Relations.Discrete][]).

```agda
compatible : (𝑨 : Algebra Ξ±) β†’ BinRel ∣ 𝑨 ∣ ρ β†’ Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ)
compatible  𝑨 R = βˆ€ 𝑓 β†’ (𝑓 Μ‚ 𝑨) |: R

compatible-pred : (𝑨 : Algebra Ξ±) β†’ Pred (∣ 𝑨 ∣ Γ— ∣ 𝑨 ∣)ρ β†’ Type (π“ž βŠ” π“₯ βŠ” Ξ± βŠ” ρ)
compatible-pred  𝑨 P = βˆ€ 𝑓 β†’ (𝑓 Μ‚ 𝑨) |:pred P
```

Recall, the `|:` type was defined in [Legacy.Base.Relations.Discrete][] module.


#### <a id="compatibility-of-continuous-relations">Compatibility of continuous relations</a>

In the [Legacy.Base.Relations.Continuous][] module, we defined a function called
`compatible-Rel` to represent the assertion that a given continuous relation is
compatible with a given operation. With that, it is easy to define a function,
which we call `compatible-Rel-alg`, representing compatibility of a continuous
relation with all operations of an algebra.  Similarly, we define the analogous
`compatible-REL-alg` function for the (even more general) type of *dependent
relations*.

```agda
module _ {I : Type π“₯} where

 compatible-Rel-alg : (𝑨 : Algebra Ξ±) β†’ Rel ∣ 𝑨 ∣ I{ρ} β†’ Type(π“ž βŠ” Ξ± βŠ” π“₯ βŠ” ρ)
 compatible-Rel-alg 𝑨 R = βˆ€ (𝑓 : ∣ 𝑆 ∣ ) β†’  compatible-Rel (𝑓 Μ‚ 𝑨) R

 compatible-REL-alg : (π’œ : I β†’ Algebra Ξ±) β†’ REL I (Ξ» i β†’ ∣ π’œ  i ∣) {ρ} β†’ Type _
 compatible-REL-alg π’œ R = βˆ€ ( 𝑓 : ∣ 𝑆 ∣ ) β†’  compatible-REL (Ξ» i β†’ 𝑓 Μ‚ (π’œ i)) R
```