Skip to main content
added 318 characters in body
Source Link
Tim Campion
  • 64k
  • 13
  • 143
  • 384

First, a clarification: what are the morphisms of locally cartesian closed categories meant to be?

Now, a word on the "two adjoints" thing.

For every category $C$, there is a cocartesian fibration $\mathrm{cod}: C^{\Delta[1]} \to C$ with fiber $C/c$ over $c \in C$; reindexing is given by composition. $C$ has pullbacks if and only if $\mathrm{cod}$ is simultaneously a cartesian fibration (i.e. it is a bifibration); reindexing is given by pullback.

If $C$ has pullbacks, then the cartesian fibration $\mathrm{cod}$ classifies a functor $C^\mathrm{op} \to \mathsf{Cat}$. This functor is also classified by a cocartesian fibration $\overline{\mathrm{cod}}: E \to C^\mathrm{op}$ (different from $\mathrm{cod}$). In the "total category" $E$, an object over $c \in C^\mathrm{op}$ is a map $f: d \to c$ in $C$, while a morphism from $f$ to $f'$ over $\gamma: c \leftarrow c'$ is a map $c \times_d c' \to d'$. Now $C$ is locally cartesian closed if and only if the cocartesian fibration $\overline{\mathrm{cod}}$ is simultatneously a cartesian fibration. Pavlovic calls such a functor a "trifibration"; his paper is referenced in the nlab page on bifibrations linked to above.

The process of straightening a cartesian fibration and then unstraightening it to get a cocartesian fibration may sound unwieldy in the $\infty$-categorical setting, but it has been studied by Barwick, Glasman, and Nardin, and I think they give a more direct construction.

Upshot:

This allows one to check that (small) locally cartesian closed categories form a presentable category, since they lie in a pullback diagram of accessible right adjoints between such:

$\require{AMScd} \begin{CD} Cat^{lcc} @>>> Cat^{cart} \\ @VVV @VVV\\ Cat^{pb} @>>> Cat^{\Delta[1]} \end{CD}$

First, a clarification: what are the morphisms of locally cartesian closed categories meant to be?

Now, a word on the "two adjoints" thing.

For every category $C$, there is a cocartesian fibration $\mathrm{cod}: C^{\Delta[1]} \to C$ with fiber $C/c$ over $c \in C$; reindexing is given by composition. $C$ has pullbacks if and only if $\mathrm{cod}$ is simultaneously a cartesian fibration (i.e. it is a bifibration); reindexing is given by pullback.

If $C$ has pullbacks, then the cartesian fibration $\mathrm{cod}$ classifies a functor $C^\mathrm{op} \to \mathsf{Cat}$. This functor is also classified by a cocartesian fibration $\overline{\mathrm{cod}}: E \to C^\mathrm{op}$ (different from $\mathrm{cod}$). In the "total category" $E$, an object over $c \in C^\mathrm{op}$ is a map $f: d \to c$ in $C$, while a morphism from $f$ to $f'$ over $\gamma: c \leftarrow c'$ is a map $c \times_d c' \to d'$. Now $C$ is locally cartesian closed if and only if the cocartesian fibration $\overline{\mathrm{cod}}$ is simultatneously a cartesian fibration. Pavlovic calls such a functor a "trifibration"; his paper is referenced in the nlab page on bifibrations linked to above.

The process of straightening a cartesian fibration and then unstraightening it to get a cocartesian fibration may sound unwieldy in the $\infty$-categorical setting, but it has been studied by Barwick, Glasman, and Nardin, and I think they give a more direct construction.

First, a clarification: what are the morphisms of locally cartesian closed categories meant to be?

Now, a word on the "two adjoints" thing.

For every category $C$, there is a cocartesian fibration $\mathrm{cod}: C^{\Delta[1]} \to C$ with fiber $C/c$ over $c \in C$; reindexing is given by composition. $C$ has pullbacks if and only if $\mathrm{cod}$ is simultaneously a cartesian fibration (i.e. it is a bifibration); reindexing is given by pullback.

If $C$ has pullbacks, then the cartesian fibration $\mathrm{cod}$ classifies a functor $C^\mathrm{op} \to \mathsf{Cat}$. This functor is also classified by a cocartesian fibration $\overline{\mathrm{cod}}: E \to C^\mathrm{op}$ (different from $\mathrm{cod}$). In the "total category" $E$, an object over $c \in C^\mathrm{op}$ is a map $f: d \to c$ in $C$, while a morphism from $f$ to $f'$ over $\gamma: c \leftarrow c'$ is a map $c \times_d c' \to d'$. Now $C$ is locally cartesian closed if and only if the cocartesian fibration $\overline{\mathrm{cod}}$ is simultatneously a cartesian fibration. Pavlovic calls such a functor a "trifibration"; his paper is referenced in the nlab page on bifibrations linked to above.

The process of straightening a cartesian fibration and then unstraightening it to get a cocartesian fibration may sound unwieldy in the $\infty$-categorical setting, but it has been studied by Barwick, Glasman, and Nardin, and I think they give a more direct construction.

Upshot:

This allows one to check that (small) locally cartesian closed categories form a presentable category, since they lie in a pullback diagram of accessible right adjoints between such:

$\require{AMScd} \begin{CD} Cat^{lcc} @>>> Cat^{cart} \\ @VVV @VVV\\ Cat^{pb} @>>> Cat^{\Delta[1]} \end{CD}$

Source Link
Tim Campion
  • 64k
  • 13
  • 143
  • 384

First, a clarification: what are the morphisms of locally cartesian closed categories meant to be?

Now, a word on the "two adjoints" thing.

For every category $C$, there is a cocartesian fibration $\mathrm{cod}: C^{\Delta[1]} \to C$ with fiber $C/c$ over $c \in C$; reindexing is given by composition. $C$ has pullbacks if and only if $\mathrm{cod}$ is simultaneously a cartesian fibration (i.e. it is a bifibration); reindexing is given by pullback.

If $C$ has pullbacks, then the cartesian fibration $\mathrm{cod}$ classifies a functor $C^\mathrm{op} \to \mathsf{Cat}$. This functor is also classified by a cocartesian fibration $\overline{\mathrm{cod}}: E \to C^\mathrm{op}$ (different from $\mathrm{cod}$). In the "total category" $E$, an object over $c \in C^\mathrm{op}$ is a map $f: d \to c$ in $C$, while a morphism from $f$ to $f'$ over $\gamma: c \leftarrow c'$ is a map $c \times_d c' \to d'$. Now $C$ is locally cartesian closed if and only if the cocartesian fibration $\overline{\mathrm{cod}}$ is simultatneously a cartesian fibration. Pavlovic calls such a functor a "trifibration"; his paper is referenced in the nlab page on bifibrations linked to above.

The process of straightening a cartesian fibration and then unstraightening it to get a cocartesian fibration may sound unwieldy in the $\infty$-categorical setting, but it has been studied by Barwick, Glasman, and Nardin, and I think they give a more direct construction.