I'm unsure if my question is advanced enough for this site, but let's see.

Let $\mathcal{C}$ be a locally cartesian closed category, so that it always has dependent products $\Pi_f$, i.e., right adjoints to base change functors $f^{\ast}$, along with dependent sums $\Sigma_f$, i.e., left adjoints to base change functors. In the article Simplicial Model of Univ. Foundations, Definition 1.4.1 is an expression $$U^{\sqcap}\equiv \underbrace{\Sigma_{U \rightarrow 1}}_{F(U)} \underbrace{\Pi_{\tilde{U} \rightarrow U}}_{G(U)}\left(\underbrace{\pi_{2}: U \times \tilde{U} \rightarrow \tilde{U}}_{H(U)}\right) $$ where $\tilde{U}\to U$ refers to a particular morphism $p$ with which $U$ comes equipped. (This morphism gives the structure of a so-called universe in $\mathcal{C}$, but this shouldn't be essential to my question.)

Now, the authors refer to the "evident functoriality" of $U^{\sqcap}$ in $U$. But I just don't see this.

$U^{\sqcap}$ has the form $F(U)(G(U)(H(U)))$ where $F$ and $G$ refer to functors defined in terms of $U$ and $H$ is a functor on pairs of objects in $\mathcal{C}$. If we are given a morphism $(f,g)$ in the arrow category of $\mathcal{C}$ from $\tilde{U}'\to U'$ to $\tilde{U}\to U$, we get an induced map $H(f,g):\pi_2' \to \pi_2$. I also believe that we can view $\Pi_{-}$ and $\Sigma_{-}$ as functors from the arrow category of $\mathcal{C}$ to the arrow category of $\text{CAT}$. But I'm getting nowhere with trying put this all together to find an induced map $(f,h)^{\sqcap}:\left(U'\right)^{\sqcap} \to U^{\sqcap}$.

I'm likely missing something obvious, but any help would be much appreciated.


You are right that $(-)^{\mathsf \Pi}$ is not functorial on the arrow category of $\mathcal{C}$. However, it is functorial on the category whose objects are arrows in $\mathcal{C}$ and whose morphisms are pullback squares, and I believe that's what the authors were referring to, since in their case $\tilde{U_0}$ is defined as the pullback of $\tilde{U}$ to $U_0$.

Given a pullback square $\require{AMScd}$ \begin{CD} \tilde{U}' @>f>> \tilde{U} \\ @V p' VV @VV p V \\ U' @>>g> U \end{CD} we have a map $\tilde{U}' \times U' \to \tilde{U} \times U$ over $f$ and hence a map $\tilde{U}' \times U' \to f^*(\tilde{U} \times U)$ over $\tilde{U}'$, thus by functoriality a map $(U')^{\mathsf{\Pi}} = \Pi_{p'}(\tilde{U}'\times U') \to \Pi_{p'}(f^*(\tilde{U}\times U))$. But by the Beck-Chevalley condition for the pullback square we have $\Pi_{p'}(f^*(\tilde{U}\times U)) \cong g^*(\Pi_p(\tilde{U}\times U)) = g^*(U^{\mathsf{\Pi}})$, so we get a map $(U')^{\mathsf{\Pi}} \to g^*(U^{\mathsf{\Pi}})$ over $U'$, hence a map $(U')^{\mathsf{\Pi}} \to U^{\mathsf{\Pi}}$ over $g$.

  • $\begingroup$ I still can't see how it would act on morphisms. Would you mind saying a bit more about what the induced map would look like? $\endgroup$ – CuriousKid7 Nov 18 at 4:12
  • $\begingroup$ @CuriousKid7 I added some details. $\endgroup$ – Mike Shulman Nov 18 at 14:18
  • $\begingroup$ Sorry, another clarification: How do you know that the Beck-Chevalley condition is satisfied? It seems from nLab that the condition holds so long as the square in our case is a pullback (which it is here). Is this fact true due to some general theorem about the Beck-Chevalley condition that I'm unaware of, or is this just a matter of direct verification? $\endgroup$ – CuriousKid7 Nov 20 at 2:27
  • $\begingroup$ @CuriousKid7 The fact that the Beck-Chevalley condition holds for any pullback square is indeed a general theorem. Probably the easiest way to prove it is to pass to left adjoints of everything and use the pullback pasting lemma. $\endgroup$ – Mike Shulman Nov 20 at 6:28
  • 1
    $\begingroup$ @CuriousKid7 Joyal's proof is of a different and much subtler Beck-Chevalley condition, involving derived Kan extensions of diagrams on quasicategories. This Beck-Chevalley condition is much simpler and can be proven in a few lines; my last comment explains how (very briefly, to be sure). I'm not sure offhand where to find this written out in more detail, but it's a nice exercise to work out yourself. $\endgroup$ – Mike Shulman Nov 20 at 17:27

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.