dependent colimits

Stream: mathlib4

[Jakob von Raumer]

So @Markus Himmel and me came across a case which might not be too rare in category theory: A theorem that on paper involves a double colimit of the form $\mathrm{colim}_{j \in J} \mathrm{colim}_{i \in I(j)} F(j, i)$. The issue with this is that we can't to denote this as a colimit (colimit _) in Lean, because the domain of the inner functor depends on the outer index, and functors are inherently non-dependent. There's been some drafts by @Junyan Xu on this, but maybe someone else has come across that specifically and found a good solution that is not too ad-hoc?

[Jakob von Raumer]

In the case were $I$ is a pseudofunctor to $\mathsf{Cat}$, we could in this just use the colimit on the Grothendieck construction, but that solution doesn't generalize to terms like $\mathrm{lim}_{j \in J} \mathrm{colim}_{i \in I(j)} F(j, i)$, for example.

[Adam Topaz]

A special case of this comes up in the definition of (left) Kan extensions, but that case was essentially handled in an "ad-hoc" way.

[Adam Topaz]

For lim colim you could use a Grothendieck construction trick by taking ops.

[Jakob von Raumer]

Do you think there's any better way than ad-hoc definitions that hide the inner colim? There's Iosif Petrakis' stuff that's linked in the other thread, but that's not commonly used it seems

[Jakob von Raumer]

Adam Topaz said:

For lim colim you could use a Grothendieck construction trick by taking ops.

Digging up that old thread. It's not that easy, because the op of a Grothendieck construction isn't a Grothendieck construction, right? Beause it's an opfibration and not a fibration