[001R] Construction 5.2·a.

Let $C$ be an internal category in $E$. We may define a fibered category $\brk{C}$ over $E$ called the externalization of $C$.

  1. Given $x\in E$, an object of $\brk{C}\Sub{x}$ is defined to be a morphism $x\to C\Sub{0}$ in $E$.

  2. Given $x,y\in E$ and $f:x\to y$ and $u \in \brk{C}\Sub{x}$ and $v\in \brk{C}\Sub{y}$, a morphism $u\to\Sub{f} v$ is defined to be a morphism $h : x\to C\Sub{1}$ in $E$ such that the following diagram commutes: