### Operations

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

For consistency and readability, we reserve two universe variables for special purposes.

The first of these is `π` which we used in the Overture.Signatures as the universe of the type of operation symbols of a signature.

The second is `π₯` which we reserve for types representing arities of relations or operations.

The type `Op` encodes the arity of an operation as an arbitrary type `I : Type π₯`, which gives us a very general way to represent an operation as a function type with domain `I β A` (the type of βtuplesβ) and codomain `A`.

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

module Overture.Operations where

-- Imports from Agda and the Agda Standard Library -----------------------------
open import Agda.Primitive               using () renaming ( Set to Type )
open import Level                        using ( Level ; _β_ )

private variable Ξ± Ξ² Ο π₯ : Level

-- The type of operations on A of arity I
Op : Type Ξ± β Type π₯ β Type (Ξ± β π₯)
Op A I = (I β A) β A

```

For example, the `I`-ary projection operations on `A` are represented as inhabitants of the type `Op A I` as follows.

```
-- Example (projections)
Ο : {I : Type π₯} {A : Type Ξ± } β I β Op A I
Ο i = Ξ» x β x i

```

Occasionally we want to extract the arity of a given operation symbol.

```
-- return the arity of a given operation symbol
arity[_] : {I : Type π₯} {A : Type Ξ± } β Op A I β Type π₯
arity[_] {I = I} f = I
```