Models of signatures

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

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

module universal-algebra.models-of-signatures where
Imports 
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.function-extensionality
open import foundation.sets
open import foundation.structure-identity-principle
open import foundation.universe-levels

open import foundation-core.cartesian-product-types
open import foundation-core.dependent-identifications
open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.identity-types
open import foundation-core.propositions
open import foundation-core.torsorial-type-families

open import lists.functoriality-tuples
open import lists.tuples

open import universal-algebra.signatures

Idea

A model of a single-sorted finitary algebraic signature σ in a type A is a dependent function that assigns to each function symbol f of arity n and n-tuple of elements of A an element of A.

Definitions

The predicate on a type of being a model

is-model-of-signature-type :
  {l1 l2 : Level} → signature l1 → UU l2 → UU (l1 ⊔ l2)
is-model-of-signature-type σ X =
  (f : operation-signature σ) →
  tuple X (arity-operation-signature σ f) → X

The predicate on a set of being a model

is-model-of-signature : {l1 l2 : Level} → signature l1 → Set l2 → UU (l1 ⊔ l2)
is-model-of-signature σ X = is-model-of-signature-type σ (type-Set X)

The type of models of a signature

Model-Of-Signature :
  {l1 : Level} (l2 : Level) → signature l1 → UU (l1 ⊔ lsuc l2)
Model-Of-Signature l2 σ = Σ (Set l2) (is-model-of-signature σ)

module _
  {l1 l2 : Level} (σ : signature l1) (X : Model-Of-Signature l2 σ)
  where

  set-Model-Of-Signature : Set l2
  set-Model-Of-Signature = pr1 X

  is-model-set-Model-Of-Signature :
    is-model-of-signature σ set-Model-Of-Signature
  is-model-set-Model-Of-Signature = pr2 X

  type-Model-Of-Signature : UU l2
  type-Model-Of-Signature = type-Set set-Model-Of-Signature

  is-set-type-Model-Of-Signature : is-set type-Model-Of-Signature
  is-set-type-Model-Of-Signature = is-set-type-Set set-Model-Of-Signature

Recent changes