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

I started a GitHub repository called UniversalAlgebra/Conferences in an effort to
keep up with the vast number of meetings in these areas and help make
summer travel plans accordingly.