Abstract equations over signatures

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

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

module universal-algebra.abstract-equations-over-signatures where
Imports 
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 = term σ × term σ

  lhs-abstract-equation : abstract-equation → term σ
  lhs-abstract-equation = pr1

  rhs-abstract-equation : abstract-equation → term σ
  rhs-abstract-equation = pr2

Recent changes