Signatures

Content created by Fernando Chu, Fredrik Bakke and Garrett Figueroa.

Created on 2023-03-20.
Last modified on 2025-10-31.

module universal-algebra.signatures where
Imports 
open import elementary-number-theory.natural-numbers

open import foundation.cartesian-product-types
open import foundation.dependent-pair-types
open import foundation.embeddings
open import foundation.identity-types
open import foundation.universe-levels

Idea

A (single-sorted, finitary, algebraic) signature is a collection of function symbols with given finite arities.

Definitions

Signatures

signature : (l : Level) → UU (lsuc l)
signature l = Σ (UU l) (λ operations → (operations → ℕ))

operation-signature : {l : Level} → signature l → UU l
operation-signature = pr1

arity-operation-signature :
  {l : Level} (σ : signature l) → operation-signature σ → ℕ
arity-operation-signature = pr2

Recent changes