agda-ualib

Archived page

This page is kept for reference and its original URL still works, but it is not part of the current site and is no longer maintained. Dates and links reflect when it was written.

(Shown above is a general formulation of composition of operations in dependent type theory, as derived here.)

This page is a teaser for the agda-ualib package and its documentation (tutorial/textbook) that we are currently developing to formalize universal algebra in the Agda functional programming language and interactive theorem prover.

• relations
• composition
• f-algebras
• elementary facts

---

The Agda Universal Algebra Library (agda-algebras) is work in progress. You can view some detailed documentation by clicking here and the agda-ualib software repository by clicking here.