🌞Summer School Announcement🌞
🎓∞-Category Theory at ICERM!🎓

I am happy to announce that together with
@emilyriehl.bsky.social and Jonathan Weinberger we are organizing a Graduate Training Workshop teaching ∞-category theory via proof assistants!🧠💻

More infos in the next post👉

This past year I spent some time thinking about filter quotient models of homotopy type theory.

I am happy to announce that I now have a chance to talk about it

📍 First Meeting of the Higher Structures Network, Nottingham, UK
🗓️ Thursday Nov. 19

Links in the next post👉

🚀 Exciting news!

I’m organizing the conference

Formalizing Higher Categories

at Institut Mittag-Leffler (Stockholm, June 2026)

— bringing together experts to explore how far ∞-category theory can be formalized in proof assistants (like Lean).

More info in the next post 👇

Every postdoc whenever fall comes around again:

#AcademicLife #JobMarket #PostDocLife

Rare #achievement unlocked:
Having 3 consecutively numbered papers on the #arXiv!

Never seen this before, so I count this as a record!

If you know of any other cases like this (or even higher) let me know!

🚨 New paper(s) alert! 🚨

In a series of 3 papers I use a technical construction (filter quotients) to contruct models of (simplicial) homotopy type theory (HoTT).

This helps better understand #formalization and possibly the role for #AI in (simplicial) HoTT.

Links in the next posts:

Concretely, we see that many explicit algebraic results, such as Morita invariance for rings and modules, manifest as a special case of very general bicategorical constructions.

I recently contributed to the FrontierMath Tier 4 Challenge from @epochai.bsky.social which aims to design an #AI benchmark for advanced mathematics:
epoch.ai/frontiermath...

I found this experience fascinating & so elaborated on it somewhat. Check it out:
www.linkedin.com/posts/nimara...

I am happy to announce that my paper joint with Niels van der Weide, Benedikt Ahrens & Paige Randall North has been published at Computer Science Logic 2025.
We show how univalent mathematics can be used to study intricate (higher) categories & formalize it in Coq UniMath
doi.org/10.4230/LIPI...