nLab flagged category

Definition

A flagged category consists of a category $C$, a groupoid $X$, and a surjection $p \colon X\to C$ of groupoids from $X$ to the underlying groupoid of objects of $C$ (hence an essentially surjective functor).

One may also call this a category with an atlas, where the atlas is allowed to be groupoidal itself.

In type theory

A flagged category is a 1-truncated precategory.

See also

• category with an atlas

• univalent category

• gaunt category

References

The terminology “flagged” for this notion appears (in generalization to higher category theory) in:

• David Ayala, John Francis, Def. 0.12 of: Flagged higher categories, in: Topology and Quantum Theory in Interaction, Contemporary Mathematics 718, AMS (2018) [arXiv:1801.08973, ISBN:978-1-4704-4941-4]