Commit 2026-06-18 10:58 cb934192
View on Github →feat(CategoryTheory): the κ-accessible category of κ-directed posets (#39655)
Given a regular cardinal κ : Cardinal.{u}, we show that the category CardinalFilteredPoset κ of κ-directed partially ordered types (with order embeddings as morphisms) is a κ-accessible category.