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 .


Some useful operations on sets and types.


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


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

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

Back to Home Page