Universal Algebra in Coq

by Venanzio Capretta

The following files are an implementation in the proof system Coq (version 6.2.3) of the basic notions and results of Universal Algebra. The development is inspired by the presentation of Universal Algebra in the article by K. Meinke and J. V. Tucker in the Handbook of Logic in Computer Science.

Download the following archive file to get all the sources of the development: universal_algebra.tar.gz

A description of the work can be found in my paper Universal Algebra in Type Theory .

Tools

Some useful operations on sets and types.

Non dependent equality
Type Constructions
Finite Sets
Type Products
Lists Projections

Setoids

Setoids are sets endowed with an equivalence relation. they serve the same purpose as the sets of set theory in classical Universal Algebra

Setoids
Parametric Arity Functions
General Trees

Algebra

Definitions of the basic notions of Universal Algebra, constructions on algebras, term algebras and basic results about them.

Signatures
Algebras
Term Algebras
Expressions Algebras
Homomorphisms
Term Evaluation
Expressions Evaluation
Subalgebras
Congruences
Kernels
First Homomorphism Theorem

Any comment or suggestion is welcome. You can e-mail me at the address venanzio@cs.kun.nl.

Back to Home Page