Contents

category theory

# Contents

## 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.