and pointer to:

- Peter Scholze, p. 11 of:
*Six Functor Formalisms*, lecture notes (2022) [pdf]

added pointer to:

- Martin Gallauer, pp. 16 of:
*An introduction to six-functor formalism*, lecture at*The Six-Functor Formalism and Motivic Homotopy Theory*, Università degli Studi di Milano (Sept. 2021) [arXiv:2112.10456, pdf]

In the (stub) section “Motivation – From logic and type theory” (here) I added more explicit pointers to the references, including page and section number .

]]>spelled out (here) a simple special case of Beck-Chevalley for enriched functor categories

]]>made fully explicit (here) the elementary example of Beck-Chevalley for images/preimages of sets — because it’s fun and because it gives already half of the proof of Beck-Chevalley for presheaf categories.

]]>To that same section I have added a remark (here) that the opfibrancy condition is to ensure that the pullback presents a 2-pullback/homotopy-pullback.

]]>I have spelled out more details in the Examples-section (here) on BC for pull-push of general functor categories through pullback diagrams of opfibrations.

]]>added pointer to:

- Simon John Ambler, §5.5.1 in:
*First Order Linear Logic in Symmetric Monoidal Closed Categories*, PhD thesis, Edinburgh (1991) [ECS-LFCS-92-194, pdf]

added pointer to:

- Michael Hopkins, Jacob Lurie, Prop. 4.3.3 in:
*Ambidexterity in K(n)-Local Stable Homotopy Theory*(2013) [pdf]

I’d like the entry to state the following fact, if it is true:

For

$V$ some cosmos for enrichment,

$S \subset VCat$ some sub-1-category of small strict $V$-categories

$\mathbf{C}$ a (co)complete closed monoidal $V$-category

then the indexed monoidal $V$-category of $\mathbf{C}$-valued (co)presheaves on the $\mathcal{X}$s

$(\mathcal{X} \in S) \mapsto V Func( \mathcal{X} ,\, \mathbf{C} )$satisfies Beck-Chevalley.

In looking through the literature for who might have said this, I find Mike’s Theorem p. 9.3 here, whose proof seems like it claims a general statement of which this is a special case, if I am unwinding the notation correctly.(?)

]]>added these pointers:

Michael Shulman,

*Comparing composites of left and right derived functors*, New York Journal of Mathematics**17**(2011) 75-125 [arXiv:0706.2868, eudml:229181]Mike Shulman,

*Framed bicategories and monoidal fibrations*, Theory and Applications of Categories,**20**18 (2008) 650–738 [tac:2018, arXiv:0706.1286]

added pointer to:

- Robert A. G. Seely,
*Hyperdoctrines, Natural Deduction and the Beck Condition*, Zeitschr. f. math Logik und Grundlagen d. Math.**29**(1983) 505-542 [pdf]

and

- Duško Pavlović,
*Maps II: Chasing Diagrams in Categorical Proof Theory*, Logic Journal of the IGPL,**4**2 (1996) 159–194 [doi:10.1093/jigpal/4.2.159, pdf]

added pointer to:

Michael Shulman, e.g. Thm. 9.3 in:

*Enriched indexed categories*, Theory Appl. Categ.**28**(2013) 616-695 [doi:1212.3914, tac:28-21]Emily Riehl, Dominic Verity, Prop. 5.3.9 in:

*Kan extensions and the calculus of modules for ∞-categories*, Algebr. Geom. Topol.**17**(2017) 189-271 [doi:10.2140/agt.2017.17.189, arXiv:1507.01460]

okay, I have now fixed the orientation of the diagrams (here)

and added also brief mentioning of the *other* main motivation for Beck-Chevalley as expressing substitution of free variables commuting with quantification over bound variables (here)

Thanks for the alert that this motivation was missing on the page. I feel like we may have this elsewhere on the nLab, but would have to check (not right now though, am just on my phone in between other thing). There is some more along these lines in “Quantization via Linear Homotopy Types”, but may not expository enough for what we’d want here.

In any case, I have rewritten the text you dropped, for better clarity. The simple point is that Beck-Chevalley is the condition to make pull-push base change through correspondences functorial under composition of correspondences by fiber product of adjacent legs.

I would also like to redo the diagrams (pity to use `xymatrix`

and then still show composition from top-right to bottom-left instead of just left to right as usual) but maybe later.

Transferred the content of an answer by Fosco Loregian.

]]>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.

]]>