University of Cambridge > > Formalisation of mathematics with interactive theorem provers  > Lawvere Theories in Lean

Lawvere Theories in Lean

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jonas Bayer.


Lawvere theories provide a categorical approach to Universal Algebra, and their models have the benefit of being easily interpreted in any category with finite products. This talk will discuss a formalization of (multi-sorted) Lawvere theories in Lean4, as well as some work in progress toward relating them to the preexisting algebraic hierarchy.


WATCH ONLINE HERE : Meeting ID: 370 771 279 261 Passcode: iCo7a5

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity