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