Signatures

Content created by Fernando Chu.

Created on 2023-03-20.

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 signature is a collection of function symbols with given 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 Sg = pr1 Sg

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


Extension of signatures

is-extension-signature :
{ l1 l2 : Level} →
signature l1 → signature l2 → UU (l1 ⊔ l2)
is-extension-signature Sg1 Sg2 =
Σ ( operation-signature Sg2 → operation-signature Sg1)
( λ f → is-emb f ×
( ( op : operation-signature Sg2) →
arity-operation-signature Sg2 op ＝
arity-operation-signature Sg1 (f op)))

emb-extension-signature :
{ l1 l2 : Level} →
( Sg1 : signature l1) →
( Sg2 : signature l2) →
is-extension-signature Sg1 Sg2 →
( operation-signature Sg2 → operation-signature Sg1)
emb-extension-signature Sg1 Sg2 ext = pr1 ext

is-emb-extension-signature :
{ l1 l2 : Level} →
( Sg1 : signature l1) →
( Sg2 : signature l2) →
( ext : is-extension-signature Sg1 Sg2) →
is-emb (emb-extension-signature Sg1 Sg2 ext)
is-emb-extension-signature Sg1 Sg2 ext = pr1 (pr2 ext)

arity-preserved-extension-signature :
{ l1 l2 : Level} →
( Sg1 : signature l1) →
( Sg2 : signature l2) →
( ext : is-extension-signature Sg1 Sg2) →
( op : operation-signature Sg2) →
arity-operation-signature Sg2 op ＝
arity-operation-signature Sg1
( emb-extension-signature Sg1 Sg2 ext op)
arity-preserved-extension-signature Sg1 Sg2 ext = pr2 (pr2 ext)