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

  Browse A-Z

Log in

Googledetails Microsoftdetails

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Lawvere Theories in Lean

Download to your calendar using vCal

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

Online

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 : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5

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

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Diversity Cinema at UIS Berridge room on L5 at the Department of Radiology, Addenbrooke's hospital Hughes Hall, Cambridge University

Other talks

CSaP Annual Cleevely Lecture 2026 Bacterial Physiology During Growth Arrest: Can It Be Targeted by Anti-Bacterial Therapeutics? Morning Break Group Work Sera Markoff Inaugural Lecture for the Plumian Professorship in Astronomy and Experimental Philosophy - 'Staring into the heart of darkness: from theory to the direct imaging of black holes' The United States of America at 250: Reflections on the Past, Present and Future of Independence
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity