Algebraic Theories

Stream: new members

[Jonathan Konig]

Hi, I’ve recently completed a project in Lean formalizing several notions of presentation invariant algebraic theories (abstract clones, Lawvere theories, length-bijective C-systems, substitution algebras, substitution monoids, and finitary monads), the associated categories, and several equivalences and isomorphisms of these categories, establishing that they are all equivalent. This involved several standard results in category theory such as the skeleton category of finite sets is finitely cocomplete, the equivalence between strongly and weakly finitary functors in the category of sets, fubini interchange of iterated ends / coends, the coend formula of the left-kan extension, etc. I was wondering if any of this might be suitable to include somewhere in Mathlib. I would be happy to provide more details / code if so.

[Yaël Dillies]

Hey! That sounds very interesting. Let me ping a few relevant people: @Sina Hazratpour, @Aaron Anderson, @Adam Topaz

[Alex Meiburg]

I would love to see your implementation of abstract clones! I tried one a while ago but it kind of stalled out in the review process, it was sad.

[Jonathan Konig]

Great, thanks. You can check out the project on my GitHub! This was my first time using Lean so there is definitely lots of room for improvement.