Added intuition for why the Grothendieck construction is an equivalence for groupoids.

Owen Lynch

]]>added the observation (here) that

for a pseudofunctor

$\mathbf{D}^{op} \overset{C_{(-)}}{\longrightarrow} Cat$and an adjunction

$\mathcal{D} \underoverset {\underset{R}{\longleftarrow}} {\overset{L}{\longrightarrow}} {\;\; \bot \;\;} \mathbf{D}$there is an induced covering adjunction between the Grothendieck constructions

$\Big( \underset {x \in \mathcal{D}} {\textstyle{\int}} C_{L(x)} \Big) \; \underoverset {\underset{\widehat R}{\longleftarrow}} {\overset{\widehat L}{\longrightarrow}} {\;\; \bot \;\;} \; \Big( \underset {\mathbf{x} \in \mathbf{D}} {\textstyle{\int}} C_{\mathbf{x}} \Big)$ ]]>In the section of (co)limits *in* a Grothendieck construction (here) I have made explicit the example of the Cartesian product (here), which comes out as the “external cartesian product” on the fiber categories.

added pointer to what I suppose is the original reference:

- Alexander Grothendieck, §VI.8 of:
*Revêtements Étales et Groupe Fondamental - Séminaire de Géometrie Algébrique du Bois Marie 1960/61*(SGA 1) , LNM**224**Springer (1971) [updated version with comments by M. Raynaud: arxiv.0206203]

In the section “(Co)Limits in a Grothendieck construction” (here) — which used to just state sufficient conditions for (co)limits to exist, I added an indication of how they are actually computed under these conditions.

(May try to harmonize notation with the previous material tomorrow.)

]]>https://ncatlab.org/nlab/show/Grothendieck+construction#other_like_constructions_for_categories

which contains a tangible construction (rather than a proposition), which comes from the note. The necessity to cite one's sources would imply the removal of that section as well. ]]>

It may be unclear what it means to label a mathematical text as controversial.

How about, instead, you first develop your note to the point that it contains a tangible proposition; and then we check it out to put it back on the nLab?

]]>I think there is a lot to disagree with in the note under discussion, not only in the discussion of the “flaws” of the Grothendieck construction, but also in the discussion of self-classification (it is clear that not everything can be classified by a big version of itself! That does not mean it isn’t a wonderful thing when it is possible, and allusions to modes do not change this.). Everyone is certainly entitled to their opinion, and there are some interesting points made in there, but maybe for the nlab, I strongly think we should avoid taking on board such controversial viewpoints that seem to be deeply speculative.

]]>Regarding flaw 1.9, if I recall correctly, my experience has been in the other direction: that the majority of usage is for the Grothendieck construction for contravariant functors, although not to the point I would consider the covariant Grothendieck construction’s usage to be rare. E.g. it’s invoked to establish equivalences between Grothendieck fibrations and contravariant Cat-valued pseudofunctors. Or Lurie’s exposition for the straightening/unstraightening construction for the equivalence between cartesian fibrations of $\infty$-categories and $\infty Cat$-valued functors.

]]>Make the note at “A Vision for Natural Type Theory” shorter again, and put a paragraph under “generalizations”.

]]>Then maybe best to move the paragraph out of the references-section at the ordinary *Grothendieck construction* (on which your claim seems at best weak to me) into the bulk of *directed type theory*, or maybe into a new entry *(n,r)-Grothendieck construction*?

(Assuming "this" refers to (infty, 1)-directed type theory at large.) ]]>

Did you see that Cisinski et al. seem to claim (here) to have sorted this out?

]]>Well I’m not sure how this would work in constructive mathematics, now that I think of it. Could you rebuild the pseudofunctor without defining a Grothendieck fibration in such a way that it is actually a cloven one? This page suggests that without cleavage, you can merely build a pseudofunctor to the 2-category of categories, anafunctors, and ananatural transformations. Without cleavage and with choice, you can rebuild the pseudofunctor, but its computational content may differ from the original one when considered on the nose.

]]>Rephrase exposition for reference to “Grothendieck Construction Considered Harmful”.

]]>Regarding flaw 1.10: I state "Indeed, in the GF, we can recognize cartesian arrows, which are arrows that can serve as mappings of the functorial action of D. However, these mappings are not unique on the nose." They are of course unique up to isomorphism, and so the pseudofunctor can be reinstated up to 2-equivalence (?), but not up to equality. The computational content of the original pseudofunctor's action on 1-cells has been discarded and new computational content for the reinstated pseudofunctor needs to be derived from the computational content of the proof of being a Grothendieck fibration (if that property has been stated in such a way that it contains computational content), (edit: or from the axiom of choice), which may not lead to the same outcome on the nose.

I will rephrase the remark. ]]>

Looking closer at your note now.

You claim to see two “flaws” of the Grothendieck construction, “Flaw 1.9” (p. 4) and “Flaw 1.10” (p. 5).

It seems that “flaw 1.9” comes down to the feeling that

the GC and the twisted GC are equally panthodic, yet the twisted GC is rarely used, if ever. This should indicate that something is off.

But just a few lines above you note that what you call the “twisted GC” is “an instance of the GC.” This seems to render the previous “flaw” a moot point by your own account, no?

$\,$

In “flaw 1.10” you claim that

it is still impossible to reconstruct $\mathcal{D}$ [a pseudofunctor] from the GF $\big(\int_{\mathcal{C}} \mathcal{D}, \pi_1\big)$ [its associated Grothenieck fibration]

This seems to directly contradict the first and constituting fact about the Grothendieck construction (here).

]]>Sounds interesting. How about adding a comment to this effect to the entry, so that the mystery is resolved a little.

I gather instead of saying

A call to think twice before using a Grothendieck construction

it might be appropriate to say

]]>For a discussion of constructions closely related to but different from the Grothendieck construction, see…

You say in the entry:

A call to think twice before using a Grothendieck construction

This sounds mysterious. Briefly scanning over the note, I am getting the impression that what you have in mind are issues you ran into when considering categorical semantics of some kind of directed type theory?

]]>Cite “Grothendieck Construction Considered Harmful”

]]>