agda-ualib

Introducing the Agda Universal Algebra Library

Reading time: less than a minute (113 words).

(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 detailed documentation (tutorial/textbook) that we are currently developing to formalize important parts of universal algebra in the Agda functional programming language and interactive theorem prover.

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