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`

. For example, the `I`

-*ary
projection operations* on `A`

are represented as inhabitants of the type `Op I A`

as
follows.

{-# 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 -- Example (projections) Ο : {I : Type π₯} {A : Type Ξ± } β I β Op A I Ο i x = x i -- return the arity of a given operation symbol arity[_] : {I : Type π₯} {A : Type Ξ± } β Op A I β Type π₯ arity[_] {I = I} f = I