Added reference to exact square. More generally, it might be preferable to give this condition a more descriptive name, especially when the contribution of Beck to the definition of this condition is disputed (for instance, see the discussion on the categories mailing list in November 2007).

]]>finally for discussion in the generality of $\infty$-categories:

Urs Schreiber, around Def. 5.5 of:

*Quantization via Linear homotopy types (schreiber)*[arXiv:1402.7041]Dennis Gaitsgory, Jacob Lurie, Section 2.4.1 of:

*Weil’s conjecture for function fields*(2014-2017) [“first volume of expanded account” pdf]

added pointer also to:

- William Lawvere, p. 8 of:
*Equality in hyperdoctrines and comprehension schema as an adjoint functor*, Proceedings of the AMS Symposium on Pure Mathematics XVII (1970) 1-14 [pdf]

added pointer also to

- Duško Pavlović, Section 1 of:
*Categorical interpolation: Descent and the Beck-Chevalley condition without direct images*, in:*Category Theory*, Lecture Notes in Mathematics**1488**(1991) [doi:10.1007/BFb0084229, pdf]

together with this quote:

]]>The Beck-Chevalley condition has arisen in the theory of descent - as developed from Grothendieck 1959. Jon Beck and Claude Chevalley studied it independently from each another. […] It is conspicuous that neither of them ever published anything on it. [Pavlović 1991, §14]

This is better:

- Paul Balmer, around §7.5 of:
*Stacks of group representations*, J. European Math. Soc.**17**1 (2015) 189-228 [arXiv:1302.6290, doi:10.4171/jems/501]

The list of references in *Beck-Chevalley condition* is unsatisfactory. Is there some textbook or similar which reviews/discusses the issue in some generality for a general audience?

Searching, I have found

- Marino Gran, Diana Rodelo,
*Beck-Chevalley condition and Goursat categories*, Journal of Pure and Applied Algebra**221**10 (2017) 2445-2457 [arXiv:1512.04066, doi:10.1016/j.jpaa.2016.12.031]

which I have added now to the list. But this is not what I am looking for (it’s too specialized).

]]>Ah yes, of course. Thanks.

]]>The nice thing about type theory is that commutativity of everything with substitution is built into the notation, so you don’t even need to mention it. Of course it has to be mentioned when constructing categorical semantics, but the HoTT book is always working internally to type theory.

]]>I guess I thought commutativity of substitution and dependent sum at least would show up somewhere.

]]>Presumably that’s something that could be readily shown in HoTT.

Probably, although you’d first need to define some group theory, including colimits of diagrams of abelian groups.

Has there been any further work in HoTT concerning groups actions, etc.?

I don’t know of any.

By the way, why does Beck-Chevalley not appear in the HoTT book?

Where would it go?

]]>I added Mackey’s restriction formula as an example.

Presumably that’s something that could be readily shown in HoTT. Has there been any further work in HoTT concerning groups actions, etc.? Something seemed to have started a while ago, recall the regular action thread.

By the way, why does Beck-Chevalley not appear in the HoTT book?

]]>Thanks! I have added that to the entry.

]]>What would be a quick example to show that the condition that the original square in this case be not just a pullback, but a pullback of opfibrations is a necessary condition?

$C=$ the interval category $(0\to 1)$, $D=C'=$ the terminal category, $\phi=0$, $\alpha=1$, so that $D'=\emptyset$, but $\alpha^*\phi_!$ is the identity functor.

]]>I have added a *Beck-Chevalley condition* in the section *Examples – For categories of presheaves* a pointer to Joyal’s document on quasicategories, for the corresponding statement.

What would be a quick example to show that the condition that the original square in this case be not just a pullback, but a pullback of opfibrations is a necessary condition?

Then I did a little reorganization of the entry: There used to be a subsection “Bibrations” under the section “Examples”. This subsection had its own sub-sub-section “Examples”.

So I fixed that: I moved the paragraphs on BC for bifibrations to the Definition-section (maybe some haronization is now in order there), and merged its list of Examples into the general list of examples.

]]>Yes.

]]>To check that I’m understanding: is it right that the canonical transformation is actually $F_3 \Rightarrow F_1 \circ F_2$, and the BC condition makes it invertible (and hence in particular can go the other direction)?

]]>I have added the Beck-Chevalley-setup as an example to *mate*, just to have the cross-link.

Here is a **Question**:

Suppose we have a composite diagram of Wirthmüller contexts of the form

$\array{ &&&& \mathcal{C} \\ && & {}^{\mathllap{p}_1}\swarrow && \searrow^{\mathrlap{p_2}} \\ && \mathcal{A} && && \mathcal{B} \\ & {}^{\mathllap{i_1}}\swarrow && \searrow^{\mathrlap{i_2}} && {}^{\mathllap{i_3}}\swarrow && \searrow^{\mathrlap{i_4}} \\ \mathcal{X} && && \mathcal{Y} && && \mathcal{Z} }$Then we get functors

$\mathcal{X} \stackrel{F_1 \coloneqq (i_1)_!(i_2)^\ast}{\leftarrow} \mathcal{Y} \stackrel{F_2 \coloneqq (i_3)_!(i_4)^\ast}{\leftarrow} \mathcal{Z}$and the mate construction for the top square in the above diagram gives a composition transformation (at least if the BC condition holds)

$F_1 \circ F_2 \Rightarrow F_3$where

$F_3 \coloneqq (i_1 p_1)_! (i_4 p_2)^\ast \,.$Further describing this kind of situation for longer sequences of spans of Wirthmüller contexts, which I will refrain from here in this comment, yields a “monad-oid” and its Kleisli composition, as discussed in another thread.

Does this have an established name for the above kind of situation?

]]>Added to *Beck-Chevalley condition* a remark on its interpretation *In logic / type theory*.

(This can be said more nicely and in more detail, but that’s what I have for the moment.)

]]>at *Beck-Chevalley condition* I have added an Examples-section *Pullbacks of opfibrations* with statement and proof that the diagram of presheaves induced by a pullback of a small obfibration satisfies Beck-Chevalley.