category theory code

Stream: lean4

[Tomas Skrivan]

Is anyone working on porting category theory to Lean 4 or has working code for it? I would be interested in playing with it.

I'm mainly interested in natural transformations, left and right Kan extension and probably ends and coends as they can be apparently used to construct Kan extension.

---

I want to do automatic differentiation(AD) for code with side effects and I believe that AD for code with side effects is just a Kan extension of AD for pure code along the embedding of pure code in code with side effects.

All this categorical nonsense hurts my brain and I have learned about it quite recently. So I want to usen Lean to expand all the "nonsensical" definitions and help me understand them.

[Kevin Buzzard]

Of course there are people working on porting all of mathlib to Lean 4! And there are two different flavours of category theory in there -- stuff in src/control (used by tactic-writers) and stuff in src/category_theory (used by mathematicians). Do you want the former? "Are your functors lawful" is I think the question.

[Tomas Skrivan]

Ohh, I think I was looking only at the mathlib4 repo and I could not find any category theory there and I'm not up to date on how to use the actual mathlib in Lean 4 or if it is/not possible right now.

Yes, all the stuff I'm working with is lawful.

[Kevin Buzzard]

My understanding of the port situation is that oleans are ported and you could use them right now (but you won't have "jump to definition" because there won't be a definition, and I think there are other disadvantages), but porting Lean files is still a work in progress. However my understanding is that things only get hairy port-wise once you start using fancy Lean 3 tactics which don't exist yet in Lean 4, and category theory doesn't import much. So one could ask the following concrete question: what happens when you try and port the file src/category_theory/category/basic.lean to Lean 4 using the leanfile porting tools? I don't know the answer to this, or how to check.

[Alexander Bentkamp]

It works, but it's a bit difficult to set up. Here's the setup that currently works for me: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/How.20to.20install.20mathlib4

[Tomas Skrivan]

I should at least try the approach with oleans. However, it looks like there is no Kan extension or co/ends in mathlib and defining these might be difficult for me without the direct access to the already existing source code.

As this is not a high priority for me, I'm happy to wait for a proper mathlib port.

Hmm now I remembered that @Sebastian Reichelt is doing something with categories, and even has some basic notions defined here https://github.com/SReichelt/universe-abstractions/tree/main/UniverseAbstractions/CategoryTheory but the extra layers of abstraction are a bit over my head

[Tomas Skrivan]

@Alexander Bentkamp Thanks for the setup, I will look into it!

[Adam Topaz]

We have Kan extensions in mathlib (the Lean3 version) -- see docs#category_theory.Ran and the file it's in

[Tomas Skrivan]

Great! I guess I do not know how to search mathlib doc :)