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

{-# 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, throughout the agda-algebras library,
`π`

denotes the universe level of *operation symbol* types, while `π₯`

denotes the universe
level of *arity* types.

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 type
`A`

^{Ο f} `β 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`

.

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 π₯)

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

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 `π`

.