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