Bicategory of internal categories

70 Views Asked by At

On the nlab page for internal diagrams, it's stated that given a finitely cocomplete category $\mathcal{C}$ we can form a bicategory $\mathsf{CAT}(\mathcal{C})$ of categories internal to $\mathcal{C}$ -- what exactly does this look like?

The objects of $\mathsf{CAT}(\mathcal{C})$ are presumably internal categories in $\mathcal{C}$, with morphisms between them being internal functors. What are the morphisms between parallel internal functors? Is $\mathsf{CAT}(\mathcal{C})$ a discrete bicategory?

1

There are 1 best solutions below

1
On BEST ANSWER

We can form internal natural transformations between parallel internal functors.

For internal categories $X$ and $Y$ and internal functors $f, g: X \to Y$, an internal natural transformation $\alpha: f \to g$ is a map $\alpha: X_0 \to Y_1$ such that $src \circ a$ = $f_0$ and $tgt \circ a = g_0$ (intuitively, $\alpha$ is the map that takes an object $c$ to $\alpha_c: f(c) \to g(c)$). We also need this diagram to commute:

$$ \require{AMScd} \begin{CD} X_1 @>{(g_1, \alpha \circ src)}>> Y_1 \times_{Y_0} Y_1\\ @V{(\alpha \circ tgt, f_1)}VV @VV{m}V \\ Y_1 \times_{Y_0} Y_1 @>>{m}> Y_1 \end{CD} $$

where $m$ is the composition map. This diagram expresses naturality, which you can check by looking at the case internal to $\mathcal{Set}$.

Some more information can be found in this (draft of a?) paper by David Roberts.