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


### Signatures

This is the [Overture.Signatures][] module of the [Agda Universal Algebra Library][].

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

module Overture.Signatures where

-- Imports from the Agda (Builtin) and the Agda Standard Library -----------------------
open import Agda.Primitive  using () renaming ( Set to  Type )
open import Data.Product    using ( Ξ£-syntax ; proj₁ ; projβ‚‚ )
open import Level           using ( Level ; _βŠ”_ ) renaming ( suc to lsuc )
```
-->

```agda
variable π“ž π“₯ : Level
```

The variables `π“ž` and `π“₯` are not private since, throughout the [agda-algebras][] library,
`π“ž` denotes the universe level of *operation symbol* types, while `π“₯` denotes the universe
level of *arity* types.

#### Theoretical background

In [model theory](https://en.wikipedia.org/wiki/Model_theory), the *signature*
`𝑆 = (𝐢, 𝐹, 𝑅, ρ)` of a structure consists of three (possibly empty) sets `𝐢`, `𝐹`,
and `𝑅`---called *constant symbols*, *function symbols*, and *relation symbols*,
respectively---along with a function `ρ : 𝐢 + 𝐹 + 𝑅 β†’ 𝑁` that assigns an
*arity* to each symbol.

Often (but not always) `𝑁 = β„•`, the natural numbers.

As our focus here is universal algebra, we are more concerned with the restricted
notion of an *algebraic signature* (or *signature* for algebraic structures), by
which we mean a pair `𝑆 = (𝐹, ρ)` consisting of a collection `𝐹` of *operation
symbols* and an *arity function* `ρ : 𝐹 β†’ 𝑁` that maps each operation symbol to
its arity; here, 𝑁 denotes the *arity type*.

Heuristically, the arity `ρ 𝑓` of an operation symbol `𝑓 ∈ 𝐹` may be thought of as
the "number of arguments" that `𝑓` takes as "input".

If the arity of `𝑓` is `n`, then we call `𝑓` an `n`-*ary* operation symbol.  In
case `n` is 0 (or 1 or 2 or 3, respectively) we call the function *nullary* (or
*unary* or *binary* or *ternary*, respectively).

If `A` is a set and `𝑓` is a (`ρ 𝑓`)-ary operation on `A`, we often indicate this
by writing `𝑓 : A`<sup>ρ 𝑓</sup> `β†’ A`. On the other hand, the arguments of such
an operation form a (`ρ 𝑓`)-tuple, say, `(a 0, a 1, …, a (ρf-1))`, which may be
viewed as the graph of the function `a : ρ𝑓 β†’ A`.

When the codomain of `ρ` is `β„•`, we may view `ρ 𝑓` as the finite set `{0, 1, …, ρ𝑓 - 1}`.

Thus, by identifying the `ρ𝑓`-th power `A`<sup>ρ 𝑓</sup> with the type `ρ 𝑓 β†’ A` of
functions from `{0, 1, …, ρ𝑓 - 1}` to `A`, we identify the type
`A`<sup>ρ f</sup> `β†’ A` with the function type `(ρ𝑓 β†’ A) β†’ A`.

**Example**.

Suppose `𝑔 : (m β†’ A) β†’ A` is an `m`-ary operation on `A`.

Let `a : m β†’ A` be an `m`-tuple on `A`.

Then `𝑔 a` may be viewed as `𝑔 (a 0, a 1, …, a (m-1))`, which has type `A`.

Suppose further that `𝑓 : (ρ𝑓 β†’ B) β†’ B` is a `ρ𝑓`-ary operation on `B`.

Let `a : ρ𝑓 β†’ A` be a `ρ𝑓`-tuple on `A`, and let `h : A β†’ B` be a function.

Then the following typing judgments obtain:

`h ∘ a : ρ𝑓 β†’ B` and `𝑓 (h ∘ a) : B`.


#### The signature type

In the [agda-algebras][] library we represent the *signature* of an algebraic
structure using the following type.

```agda
Signature : (π“ž π“₯ : Level) β†’ Type (lsuc (π“ž βŠ” π“₯))
Signature π“ž π“₯ = Ξ£[ F ∈ Type π“ž ] (F β†’ Type π“₯)
```

Occasionally it is useful to obtain the universe level of a given signature.

```agda
Level-of-Signature : {π“ž π“₯ : Level} β†’ Signature π“ž π“₯ β†’ Level
Level-of-Signature {π“ž}{π“₯} _ = lsuc (π“ž βŠ” π“₯)
```

A signature is a Ξ£-type, so its two components are recovered by the standard
projections `proj₁` and `projβ‚‚` (from `Data.Product`, re-exported by
[Overture.Basic][]).

Consequently, if `𝑆 : Signature π“ž π“₯` is a signature, then

* `proj₁ 𝑆` denotes the set of operation symbols, and
* `projβ‚‚ 𝑆` denotes the arity function.

If `𝑓 : proj₁ 𝑆` is an operation symbol in the signature `𝑆`, then `projβ‚‚ 𝑆 𝑓`
is the arity of `𝑓`.

#### Self-documenting projections

Bare `proj₁` / `projβ‚‚` read opaquely at signature use sites.  The following
long-form aliases are definitionally identical to the projections and are the
canonical way to name a signature's components throughout the library.  See
[ADR-002][] Β§1 for the rationale and the per-tree policy.

```agda
OperationSymbolsOf : Signature π“ž π“₯ β†’ Type π“ž
OperationSymbolsOf 𝑆 = proj₁ 𝑆

ArityOf : (𝑆 : Signature π“ž π“₯) β†’ OperationSymbolsOf 𝑆 β†’ Type π“₯
ArityOf 𝑆 f = projβ‚‚ 𝑆 f
```

The bracket projections `∣_∣` / `βˆ₯_βˆ₯` are deprecated as of v3.0 (they carry a
`WARNING_ON_USAGE` in [Overture.Basic][]); new code uses `OperationSymbolsOf` /
`ArityOf` for signature components and `proj₁` / `projβ‚‚` elsewhere.