Agda UALib ↑

Operations and Signatures

This section presents the Algebras.Signatures module of the Agda Universal Algebra Library.


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

open import Universes using (𝓀₀)

module Algebras.Signatures where

open import Relations.Extensionality public

Signature type

We define the signature of an algebraic structure in Agda like this.


Signature : (π“ž π“₯ : Universe) β†’ (π“ž βŠ” π“₯) ⁺ Μ‡
Signature π“ž π“₯ = Ξ£ F κž‰ π“ž Μ‡ , (F β†’ π“₯ Μ‡)

As mentioned in the Relations.Discrete module, π“ž will always denote the universe of operation symbol types, while π“₯ is the universe of arity types.

In the Overture module we defined special syntax for the first and second projectionsβ€”namely, ∣_∣ and βˆ₯_βˆ₯, resp. Consequently, if 𝑆 : Signature π“ž π“₯ is a signature, then ∣ 𝑆 ∣ denotes the set of operation symbols, and βˆ₯ 𝑆 βˆ₯ denotes the arity function. If 𝑓 : ∣ 𝑆 ∣ is an operation symbol in the signature 𝑆, then βˆ₯ 𝑆 βˆ₯ 𝑓 is the arity of 𝑓.

Example

Here is how we could define the signature for monoids as a member of the type Signature π“ž π“₯.


data monoid-op {π“ž : Universe} : π“ž Μ‡ where
 e : monoid-op; Β· : monoid-op

open import MGS-MLTT using (𝟘; 𝟚)

monoid-sig : Signature π“ž 𝓀₀
monoid-sig = monoid-op , Ξ» { e β†’ 𝟘; Β· β†’ 𝟚 }

Thus, the signature for a monoid consists of two operation symbols, e and Β·, and a function Ξ» { e β†’ 𝟘; Β· β†’ 𝟚 } which maps e to the empty type 𝟘 (since e is the nullary identity) and maps Β· to the two element type 𝟚 (since Β· is binary).

↑ Algebras Algebras.Algebras β†’