lean-ualib

Documentation for background theory underlying the lean-ualib

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

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

This page will collect some posts that explain the technical notation and background needed to understand our formal implementation of universal algebra in the Lean theorem proving language.


The Lean Universal Algebra Library (lean-ualib) was recently launched, so we haven't implemented very much yet. Nonetheless, the lean-ualib repository is viewable here.