```{-# OPTIONS --without-K --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 )
open import Level           using ( Level ; suc ; _β_ )

variable π π₯ : Level

```

The variables `π` and `π₯` are not private since, as mentioned earlier, throughout the agda-algebras library `π` denotes the universe level of operation symbol types, while `π₯` denotes the universe level of arity types.

### Signatures of an algebra

In 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`Ο π `β 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`Ο π with the type `Ο π β A` of functions from ```{0, 1, β¦, Οπ - 1}``` to `A`, we identify the function type `A`Ο f `β A` with the function (or βfunctionalβ) type `(Οπ β A) β A`.

Example. Suppose `π : (m β A) β A` is an `m`-ary operation on `A`, and `a : m β A` is 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 we `π (h β a) : B`.

#### Signature type

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

```Signature : (π π₯ : Level) β Type (suc (π β π₯))
Signature π π₯ = Ξ£[ F β Type π ] (F β Type π₯)

Level-of-Signature : {π π₯ : Level} β Signature π π₯ β Level
Level-of-Signature {π}{π₯} _ = suc (π β π₯)

```

In the [Base.Functions][] module of the agda-algebras library, special syntax is defined 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 `π`.