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