↑ Top

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. 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

← Overture.Signatures Base β†’