Introducing the Agda Universal Algebra Library
(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.
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.