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