Refactor Grothendieck from Pseudofunctor.Grothendieck

Stream: mathlib4

[joseph hua]

@Yiming Xu and I would like to make a PR to mathlib unifying the two existing Grothendieck constructions in mathlib. More precisely

• CategoryTheory.Grothendieck defines the Grothendieck construction on a 1-functor into Cat
• Separately CategoryTheory.Pseudofunctor.Grothendieck defines the Grothendieck construction on a pseudofunctor from a LocallyDiscrete bicategory (i.e. a 1-category promoted to a bicategory) into Cat.
• I would like to refactor the former through the latter, except also I need to redefine the latter, as it puts an "op" on the source of the pseudofunctor.

Comments and ideas welcome!

[joseph hua]

Should I first make PRs that only add the new definitions and associated lemmas, without removing the old definition? I know the convention is to make small PRs

[Joël Riou]

I am not completely sure we want to remove the op in the definition of the Grothendieck construction of a pseudofunctor. Before proceeding, I would think we should ask @Calle Sönne.

[Calle Sönne]

To me, it seems fine to remove the op. However, as for certain use cases we need the op this refactor should provide good API / results to recover the current definition easily.

[Calle Sönne]

Maybe to start with let's have both definitions, then once we are convinced that it is easy to work with the op version on top of the non-op version we can replace it.

[joseph hua]

Here are two possible approaches:

1. (not defeq) Leave the definition CatgoryTheory.Grothendieck and define an equivalence between F.Grothendieck and F.toPseudofunctor'.Pseudofunctor.Grothendieck for a 1-functor F
2. (defeq) Redefine F.Grothendieck as F.toPseudofunctor'.Pseudofunctor.Grothendieck

In both approaches we basically need to define everything twice, which is fine. The main downside of 1 is that we need to prove coherence lemmas for the equivalence. The main downside of 2 is that @[simp!] produces lemmas that are not in the best form for 1-categorical reasoning. I would like to not leak the 2-categorical definition if we use that under the hood. I am currently going with approach 2. Any suggestions on this?

[Calle Sönne]

I am actually not so familiar with the 1-categorical construction. Is it common to only want to talk about this in a 1-categorical framework (I assume yes since you are interested in bridging these two)? My possibly false assumption from before was that we only had it because the bicategory library was not developed enough.

[Calle Sönne]

I always understood that the Grothendieck construction was useful for 2 (related) reasons:

• It allows you to construct pseudofunctors without checking all the coherence conditions, instead you only have to construct some fibered category which is a 1-categorical notion.
• It allows you to talk about things that should be pseudofunctors without worrying about bicategories

So what is the interest in this construction in the 1-categorical setting? The two points above no longer apply since functors are quite simple in comparison.

(this is coming from someone who just knows about these things from the point of view of stacks)

[Calle Sönne]

I am also asking these things to better understand the use case, so I can know which of the two options above would be better

[joseph hua]

So firstly, I guess you are convinced that IF there is an application of the 1-categorical version, then we should have API for both versions. My reason for believing this is that, although the 2-cells are kind of still hanging about, it is still much easier to work with the 1-categorical construction. Having worked on both the last couple of days, I'm more confident that this is true.

As for applications:
The Grothendieck construction on a 1-functor F : C -> Cat is an explicit construction of the pullback of the "universal (something) fibration", which is the forgetful functor from PCat, the category of pointed categories (homs preserve the point only up to iso) to Cat.

Specifically for my use case, PCat can be used to model a universe for dependent type theory, and the Grothendieck construction can be used to model (coherent) context extension. (Coherent means that we are relying on an explicit construction that satisfies some naturality, rather than just picking a pullback using choice.) I'm not sure about other applications of the pullback result.

For context, this is for the HoTTLean project

[joseph hua]

By the way, the pullback result is really evil, and may be something mathlib would not accept - I don't know what the consensus on this is right now. It is treating Cat as an object in the 1-category of categories. An equality between maps in the pullback diagram is an equality between functors with codomain Cat

[Fernando Chu]

Side note on the last comment: every 1-pullback in Cat is also a 2-pullback; so it doesn't seem that evil to me. Though I agree that the result in the last sentence is indeed "evil".

[joseph hua]

Nice to see you here @Fernando Chu :smile:

[Fernando Chu]

Same! :D

[joseph hua]

Oh and for further context, for a specific definition I wanted to make, I needed the result that a pseudonatural transformation between two 1-functors into Cat induces a functor between their Grothendieck constructions, which is a direct result of Pseudofunctor.Grothendieck.map

[Robin Carlier]

Fernando Chu said:

Side note on the last comment: every 1-pullback in Cat is also a 2-pullback; so it doesn't seem that evil to me. Though I agree that the result in the last sentence is indeed "evil".

I thought that's only true if one of the functor is an isofibration? At least, I'm pretty sure the 1-pullback of the two (unique) functors * -> BG is not a 2-pullback.
In the case of the universal Grothendieck construction of the identity functor (so, PCat to Cat), it's true though.

[Fernando Chu]

@Robin Carlier my claim comes from here, maybe I should clarify that by 2-pullback I mean strict 2-pullback, which is the right notion from the enriched category theory perspective (but the wrong one from the bicategory theory perspective).

[Robin Carlier]

Ok, then I understand the claim a bit more, though for "non-evil" things we want pullbacks in the bicategorical sense. Related: my PRs about what I call the "Categorical pullback" (i.e the actually bicategorical pullback) are getting merged, but I don't expect that this API can be used as it is for a nice claim about the Grothendieck construction (of pseudofunctors) being a pullback of a universal cocartesian fibration (which is what we would actually want here) for now.

[joseph hua]

I have made an initial PR here, just changing the name of Pseudofunctor.Grothendieck to Pseudofunctor.coGrothendieck. Next I will add the new definition Pseudofunctor.Grothendieck with variance consistent with the 1-categorical version.

[joseph hua]

Hi folks, I have just updated the PR again because of a conflict. Would someone mind taking a minute to approve it? From Joel's comment it seems to be good to go.