Agda UALib β

Operations and Signatures

This section presents the Algebras.Signatures module of the Agda Universal Algebra Library.

```
{-# OPTIONS --without-K --exact-split --safe #-}

open import Universes using (π€β)

module Algebras.Signatures where

open import Relations.Extensionality public

```

Signature type

We define the signature of an algebraic structure in Agda like this.

```
Signature : (π π₯ : Universe) β (π β π₯) βΊ Μ
Signature π π₯ = Ξ£ F κ π Μ , (F β π₯ Μ)

```

As mentioned in the Relations.Discrete module, π will always denote the universe of operation symbol types, while π₯ is the universe of arity types.

In the Overture module we defined special syntax for the first and second projectionsβnamely, β£_β£ and β₯_β₯, resp. Consequently, if `π : Signature π π₯` is a signature, then β£ π β£ denotes the set of operation symbols, and β₯ π β₯ denotes the arity function. If π : β£ π β£ is an operation symbol in the signature π, then β₯ π β₯ π is the arity of π.

Example

Here is how we could define the signature for monoids as a member of the type `Signature π π₯`.

```
data monoid-op {π : Universe} : π Μ where
e : monoid-op; Β· : monoid-op

open import MGS-MLTT using (π; π)

monoid-sig : Signature π π€β
monoid-sig = monoid-op , Ξ» { e β π; Β· β π }

```

Thus, the signature for a monoid consists of two operation symbols, `e` and `Β·`, and a function `Ξ» { e β π; Β· β π }` which maps `e` to the empty type π (since `e` is the nullary identity) and maps `Β·` to the two element type π (since `Β·` is binary).