Total category

Consider a displayed category $𝖣 ⇥ 𝖢$ . In order to return to the realm of ordinary category theory, we may construct the total category $\int 𝖢 𝖣$ defined as follows: #m/def/cat/dis

an object $(𝑎, 𝑥) \in \int 𝖢 𝖣$ is a pair consisting of an object $𝑎 \in 𝖢$ and an object $𝑥 \in 𝖣 𝑎$ over $𝑎$ , so that $(\int 𝖢 𝐷) 0 : = ∐ 𝑎 \in 𝖢 0 𝖣 𝑎$
a morphism $(𝑓, ¯ 𝑓) : (𝑎, 𝑥) \to (𝑏, 𝑦)$ is a pair where $𝑓 \in 𝖢 (𝑎, 𝑏)$ and $¯ 𝑓 \in 𝖣 𝑓 (𝑥, 𝑦)$ , so that $(\int 𝖢 𝖣) ((𝑎, 𝑥), (𝑏, 𝑦)) = ∐ 𝑓 \in 𝖢 (𝑎, 𝑏) 𝖣 𝑓 (𝑥, 𝑦)$
composition and identities are induced from those of $𝖢$ and $𝖣$ in the straightforward way, and similarly for the axioms.

This is naturally equipped with a “forgetful functor”

𝜋 𝖣 1 : \int 𝖢 𝖣 \to 𝖢 .

and indeed one can give an equivalence between pairs $(𝖣, 𝜋 𝖣 1)$ and displayed categories $𝖣 ⇥ 𝖢$ .

#state/tidy | #lang/en | #SemBr