AWFS in Lean

Stream: lean4

[Sina]

I have started formalizing Algebraic Weak Factorization Systems (AWFS) in Lean. So far I have done some basic stuff in Lean3 taking advantage of the category theory library there. Unfortunately, I have not followed how much category theory there is in Lean4, where can I find about this? Does it make sense to directly formalize AWFS directly in Lean4? I need adjunctions, mondas, and comondas, algebras and coalgebras, double categories, and limit/colimit stuff. Most of these exist in Lean3, but i was wondering if a good portion of these exist in Lean4, it might make more sense to use Lean4 (which I like more).

[Marcus Rossel]

You can see which parts of category theory have been ported to Lean 4 on this website: https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Arrow.html

[Marcus Rossel]

Note that Mathlib is currently being ported to Lean 4, so sooner or later all the definitions you've used in Lean 3 will be available in Lean 4.

[Eric Wieser]

#port-dashboard can also show you how far away currently-unavailable things are

[Scott Morrison]

From your list, I would guess it is mostly ported. The sooner people come over to the light side, the better. :-)