(Co)ends in LEAN

Stream: new members

[Malthe Sporring]

Hi! I have just returned from a successful LftCM23 conference (thanks to all organizers and tutors!), where I worked on formalising (co)ends with @Silvia Properzi and @Jakob von Raumer. Now we would like to take this project to completion! An initial goal is to define the equivalence between terminal wedges and limits over the twisted arrow category, and then formalise the results in Chapter 1-2 of Coend Calculus. It would also be nice to formalise weighted (co)limits while we're at it.

The project is hosted here: https://github.com/malthefogsporring/lean-coends, and anyone is welcome to contribute.

If anyone is already working on this, please let us know! In particular, @fosco are you still working on this?

[Scott Morrison]

It would be great if you could PR this material into Mathlib! Starting early is always a good idea, so you get some review of the basic definitions, and make sure it is compatible with everything else.