Abstract equations over signatures

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

Created on 2023-03-20.
Last modified on 2026-03-22.

module universal-algebra.abstract-equations-over-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.universe-levels

open import universal-algebra.signatures
open import universal-algebra.terms-over-signatures

Idea

An abstract equation over a single-sorted finitary algebraic signature σ is a statement of the form “x equals y”, where x and y are terms over σ. Thus, the data of an abstract equation is simply two terms over a common signature.

Definitions

Abstract equations

module _
  {l1 : Level} (σ : signature l1)
  where

  abstract-equation : UU l1
  abstract-equation = Σ ℕ (λ k → term σ k × term σ k)

module _
  {l : Level} (σ : signature l) ((k , lhs , rhs) : abstract-equation σ)
  where

  arity-abstract-equation : ℕ
  arity-abstract-equation = k

  lhs-abstract-equation : term σ arity-abstract-equation
  lhs-abstract-equation = lhs

  rhs-abstract-equation : term σ arity-abstract-equation
  rhs-abstract-equation = rhs

Recent changes