infinity-cosmos project synchronous meeting!

Stream: Infinity-Cosmos

[Emily Riehl]

@Mario Carneiro had the idea of scheduling a meeting for folks interested in discussing the current status and future prospects of the infinity-cosmos project. I can give a brief overview of where we are currently and what our medium term goals are. Then @Dom Verity, @Mario Carneiro, and I can answer questions, and we can discuss strategy for attacking certain short term goals.

If you're interested in attending fill your availability here (target dates Monday May 19 -- Wednesday May 28) by 6pm EDT on Sunday May 18th:

https://www.when2meet.com/?30593658-zjqkx

At that point, I'll select a slot or two that seems to work best for the group as a whole and announce the meeting.

[Emily Riehl]

Feel free to discuss any of the above topics here. We can do the Q&A asynchronously and in advance if people prefer.

[Emily Riehl]

@Jack McKoen it would be great to get an update on your work, if you're willing to give us a report. If @Nima Rasekh or @Jon Eugster or @Julian Komaromy or anyone working on or who has recently completed something they'd like to report on that would be great too.

[Jack McKoen]

Sure, I'd be happy to give a report! For now, I can say I'm close to being done, with some technical details to work on and a few sorries.

[Jon Eugster]

Im afraid I'm not that invested after all and I'll be taking up a job outside academia soon, so I don't think I'll have anything to report.

[Julian Komaromy]

Unless someone else wants to step in, I will likely be working on the 2-truncated goals (#104, ...) in a few weeks time; I just didn't want to claim it yet because of limited time to work on it.

[Emily Riehl]

Jon Eugster said:

Im afraid I'm not that invested after all and I'll be taking up a job outside academia soon, so I don't think I'll have anything to report.

No problem and congrats! Would you like someone to adopt your open PRs or would you rather keep working on them yourself?

[Nima Rasekh]

Hey @Emily Riehl thanks for tagging me!
I'd be happy to attend to get a sense what people have been up to.
I don't think I would be able to say much myself, but just because it's challenging making the time. Probably my fault, but (hopefully) also because @Matej Penciak has also been busy?
Anyway, I did fill out the poll, but if you end up not being able to pick a time that works for me, I would understand.

[Matej Penciak]

Yeah I've been in a similar boat to @Nima Rasekh , I've been fairly busy with work... But I also signed up for times for the meeting in case they work for other people

[Jon Eugster]

Emily Riehl said:

Would you like someone to adopt your open PRs or would you rather keep working on them yourself?

If somebody wants to push them along that might be quicker and certainly appreciated. I'll still try toreturn to them in a free minute otherwise

[Emily Riehl]

Save the date: we'll hold our synchronous meeting from 9am-11am EDT / 1pm-3pm UTC / 3pm-5pm CEST on Wednesday, May 28th.

In the first hour, I'll give an overview of the current status, and @Jack McKoen and anyone else who wants to present can give an update on their current work.

In the second hour, those who want to stick around can participate in some live formalization on a topic TBD. I'm hoping @Mario Carneiro will drive ;)

Questions, comments, suggestions? Let me know here.

[Kim Morrison]

Just advertising the <timezone tag: the meeting is at 2025-05-28T23:00:00+10:00 - 2025-05-29T01:00:00+10:00.

[Mario Carneiro]

(it's actually <time)

[Emily Riehl]

Tomorrow (Wednesday) we are having a synchronous meeting of the infinity-cosmos project at 2025-05-28T23:00:00+10:00 - 2025-05-29T01:00:00+10:00 in the following zoom room:

https://zoom.com/my/infinite.cosmos

All are welcome, if you'd like to hear more about near term future plans, share what you've been up to, or just hang out.

[Mario Carneiro]

starting now!

[Emily Riehl]

For those who missed it, a rough transcript of the meeting can be found here. We also had an update from @Jack McKoen with some beautiful obsidian slides that perhaps he'd like to share?

[Emily Riehl]

We have three broad open projects, all of which are independent:

(i) fill in the remaining sorries on mathlib PR #25010; see the thread "challenge: eight sorries away from product-preserving" for more discussion

(ii) fill in the sorries in the file linked above (and below), in particular proving the a Cat-enriched category defines a strict bicategory

https://github.com/emilyriehl/infinity-cosmos/blob/main/InfinityCosmos/ForMathlib/InfinityCosmos/Goals.lean

Once (i) and (ii) are complete, we will have a strict bicategory of quasicategories that we can PR directly into mathlib.

(iii) work on redeveloping the homotopy category functor for quasicategories. @Rida Hamadani and @Julian Komaromy are working on this. This, plus @Jack McKoen's work on functor quasi-categories, will be essential for understanding the 2-cells in the bicategory defined above.

[Emily Riehl]

Update: @Mario Carneiro completed the proof that a Cat-enriched category defines a bicategory!! See here: #25287

[Emily Riehl]

Item (ii) above isn't quite complete. To apply this to QCat, in addition to completing (i), we need to show that a product preserving functor between cartesian monoidal categories defines a lax monoidal functor. So if someone wants to investigate that (which might be in mathlib, that would be very helpful). But we made excellent progress today. Well done everyone.