is the equivalence of Grothendieck construction correct? about agda-categories HOT 14 CLOSED

i have a feeling that Grothendieck construction only works for functors to strict categories. consider the following construction:

C is category 2 with propositional equality. functor F is defined by mapping A to category 1 and B to this category with objects X and Y. the latter category is generated by a loop space over X and another morphism h from X to Y.

the functor Ff maps the only object in category 1 to X.

now, consider the natural isomorphism constructed by refl proof in C. the natural isomorphism α has the only index * and the morphism is Ω from the loop space. indeed, α is naturally isomorprhic. but then, in non-strict Cats, it seems to me the Grothendieck construction would require h ∘ Ω = h, which is not true.

from agda-categories.

[Slowly catching up on older stuff]
Great summary. I think it makes sense to have part of the categories library be with K. But the organization of that is tricky. I'll open a separate issue.

from agda-categories.

mumble mumble (op)fibration mumble but not bifibration, maybe? In any case, I'll look.

from agda-categories.

I agree with @HuStmpHrrr. Just arrived at the same conclusion (then discovered this issue).

from agda-categories.

Thanks for pushing this back up my priority list. What is wrong will be interesting, as Agda currently is happy with everything.

from agda-categories.

What is wrong will be interesting, as Agda currently is happy with everything.

Once you add equality for the second component (up to natural iso), the associativity and unit laws become a good deal more involved. To prove them, you need coherence constraints, which turn out to be missing.

My guess is you can either you go strict or make F a pseudofunctor.

from agda-categories.

... and why would you need the second component of the equality? Because without it, Grothendieck (constant D) is not equivalent to D.

from agda-categories.

in the old library, the construction maps to Cats in which the equivalence of functors is the more set theoretic equivalence, which would subsequently requires K. I guess I raised this point a few times already. I think one of the main contributions of this library is to explicitly distinguish what results require K and what not, so the consequences of K are definitely worth investigating. this is very hard to detect in traditional settings but becomes very obvious when working with ITT.

from agda-categories.

So I have serious doubts that Grothendieck (constant D) is equivalent to D: I believe that it is instead equivalent to C x D. As Wikipedia says, the construction remembers whence things came from. And that proof is indeed quite easy.

from agda-categories.

I believe that it is instead equivalent to C x D.

Ah yes, you're right, of course.

I was silently assuming C to be the one-object category. The point being that we can set things up in such a way that the equality on the second coordinate is all that matters.

from agda-categories.

Proposed fix in #48.

Some comments:

• I mechanized the version for pseudofunctors (rather than functors into StrictCats) since it's more general.
• The fixed version turned out a lot more complicated than the broken one.
• Interestingly, because of the way the coherence conditions are defined in Pseudofuctor, it was easier to prove the contravariant version of the construction.
• I did not prove that Grothendieck (constant D) is equivalent to C x D — exercise for the reader 😉

@HuStmpHrrr

in the old library, the construction maps to Cats in which the equivalence of functors is the more set theoretic equivalence, which would subsequently requires K.

I just want to point out that it should be easy to give the construction for (1-)functors into StrictCats without requiring any use of K!

from agda-categories.

@HuStmpHrrr

I just want to point out that it should be easy to give the construction for (1-)functors into StrictCats without requiring any use of K!

I take that back. You were correct, it seems that K is indeed necessary to instantiate the current (weak) construction to the strict case. Sorry about that.

from agda-categories.

@HuStmpHrrr

I just want to point out that it should be easy to give the construction for (1-)functors into StrictCats without requiring any use of K!

I take that back. You were correct, it seems that K is indeed necessary to instantiate the current (weak) construction to the strict case. Sorry about that.

yeah, that's how I feel. if set theory is necessary in some theorems, then K must be necessary in those cases to kill off higher-groupoid structures and bring everything back to set(in HoTT's sense). in the case of functor equality, I suppose K should be used to represent heterogeneous equality between morphisms in the codomain category.

from agda-categories.

in the case of functor equality, I suppose K should be used to represent heterogeneous equality between morphisms in the codomain category.

Actually, it's more subtle. There are no heterogeneous equalities involved, only homogeneous ones. But the problem is indeed the higher groupid structure.

One way to prove the Grothendieck construction for functors into StrictCats, is to "instantiate" the version for bicategories, like so:

1. show that every category C can be lifted to a bi-category (this is what the module 1-Category implements);
2. show that every functor F : Functor C D can be lifted to a pseudofunctor 1-Functor F : Pseudofunctor (1-Category C) (1-Category D) (I have a PR for this coming up);
3. show that there is an "inclusion" functor Inc from StrictCats to Cats (as a bicategory);
4. to obtain the Grothendieck construction for functors F : Fucntor C StrictCats as Grothendieck (Inc ∘F 1-Functor F).

The problem arises in step 3. There you have to prove that, given two (strictly) equal functors F and G, two arbitrary proofs p q : F ≡F G of that equality induce the same natural isomorphism. In an extensional or proof-irrelevant setting this is a trivial proof. There is only one way to prove equality, and only one natural iso that corresponds to it (the identity NT). But in an intensional setting without K, we simply cannot prove this.

from agda-categories.