feat(CategoryTheory): the κ-accessible category of κ-directed posets#39655

joelriou wants to merge 5 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

joelriou:cardinal-directed-posetjoelriou/mathlib4:cardinal-directed-posetCopy head branch name to clipboard