Library UniMath.Algebra.Universal.EqAlgebras

Varieties.

Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021

This file contains a formalization of equational algebras, i.e., algebra which are models of an equation system.

Require Import UniMath.MoreFoundations.Notations.

Require Export UniMath.Algebra.Universal.Algebras.
Require Export UniMath.Algebra.Universal.Equations.

Section Varieties.

  Definition holds {σ: signature} {V: varspec σ} (a: algebra σ) (e: equation σ V) : UU
    := ∏ α , fromterm (ops a) α (eqsort e) (lhs e) =
            fromterm (ops a) α (eqsort e) (rhs e).

  Definition is_eqalgebra {σ : eqspec} (a : algebra σ) : UU
    := ∏ e: equations σ , holds a (geteq e).

  Definition eqalgebra (σ : eqspec) : UU
    := ∑ a : algebra σ , is_eqalgebra a.

  Definition algebra_of_eqalgebra {σ : eqspec}
    : eqalgebra σ → algebra σ
    := pr1.
  Coercion algebra_of_eqalgebra : eqalgebra >-> algebra.

  Definition eqalgebra_proof {σ : eqspec} (a : eqalgebra σ)
    : is_eqalgebra a := pr2 a.

  Definition make_eqalgebra {σ : eqspec} (a : algebra σ) (H : is_eqalgebra a)
    : eqalgebra σ
    := tpair is_eqalgebra a H.

End Varieties.