# 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.

## Setoids

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

## 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