The nCatLab Grothendieck construction page gives an explicit description of the oplax colimit of any functor to Cat. Can someone give me a similarly explicit description (the objects and morphisms) of an oplax limit of any functor to Cat (or a link to a page which describes it)? (I've found Reedy model structures on oplax limits, but that leaves unspecified the "'obvious' coherence conditions".)

Additionally, is there a name for such a category, analogous to "Grothendieck construction" or "category of elements"?

Context: The reason I'm interested in this is because I'm trying to formulate the categorical dependent sum and dependent product in Coq. I think the oplax (co)limit are the dependent sum/product pushed across a Yoneda-like transformation (though I'm not entirely sure that it's Yoneda). Coq's dependent sum and product are more similar to the oplax (co)limit formulation, and while nCatLab has good pages on dependent sum and dependent product, it doesn't seem to have such a page on oplax limits.

Edit: I'm looking for a description of the objects and morphisms in this category, possibly together with the composition law. Here is my guess at what the objects and morphisms are: Given a functor $F : \mathcal C \to \text{Cat}$, and letting $F_0$ denote its action on objects and $F_1$ denote its action on morphisms,

  • Objects consist of the following components

    • For each object $r \in \mathcal C$, an object $x_r \in F_0(r)$
    • For all objects $s, d \in \mathcal C$ and each morphism $m \in \text{Hom}_{\mathcal C}(s, d)$, a morphism $f_m \in \text{Hom}_{F_0(d)}((F_1(m))_0(x_s), x_d)$ (Note: This doesn't agree with Reedy model structures on oplax limits, but I can't figure out how to typecheck what's there; I've added a comment to that effect.)
    • For all $r \in \mathcal C$, a proof that $f_{\text{id}_r} = \text{id}_{x_r}$ (well, actually, that $f_{\text{id}_r}$ is equal to the isomorphism induced by the proof that $(F_1(\text{id}_r))_0(x_r) = x_r$)
    • For all $p, q, r \in \mathcal C$ and all morphisms $m_0 \in \text{Hom}_{\mathcal C}(q, r)$ and $m_1 \in \text{Hom}_{\mathcal C}(p, q)$, a proof that $f_{m_0 \circ m_1} = (F_1(m_1))_1(f_{m_0}) \circ f_{m_1}$
  • Morphisms from $(x, f)$ to $(x', f')$ consist of the following components:

    • For each object $r \in \mathcal C$, a functor $g_r : x_r \to x'_r$.
    • Some coherence condition I haven't managed to phrase yet, corresponding to the commutativity square for natural transformations.

Did I get anything wrong? (In particular, is the second component of objects right? Also, what changes for lax vs. oplax?)

  • $\begingroup$ Are you familiar with the construction of a weak limit? The oplax case is the same, but you just have to be careful with the directions of the arrows. $\endgroup$ Jul 25 '13 at 8:06
  • 1
    $\begingroup$ See J.W. Gray, Formal Category Theory 1: Adjointness for 2-Categories LNM 391, &7). THese are treated (with different name) in "Cohomologie non abélienne" (J.Giraud), ch.II. $\endgroup$ Jul 29 '13 at 18:36

The oplax limit is the category of sections for the functor from the Grothendieck construction to the base category.

The strong limit is the category of cartesian sections (every arrow in the base category gets mapped to a cartesian one).

Notice how this goes along very well with the interpretation as dependent product and as $\forall$: The set theoretic product is just the set of sections into the disjoint union.


Given a strong functor $F:X\to\mathrm{Cat}$ we denote the Grothendieck construction by $$\mathrm{Gr}(F).$$ There is a canonical functor $\pi:\mathrm{Gr}(F)\to X$. Sections of this functor are functors $$s:X\to\mathrm{Gr}(F)$$ such that $s\circ\pi=\mathrm{id}$.

So even more explicitely a section amounts to

forall $x\in X$ an object $s_x\in F(x)$ and ...

  • $\begingroup$ Is there an explicit description (describing the objects and morphisms) of the category of sections somewhere? $\endgroup$ Jul 30 '13 at 18:18
  • $\begingroup$ I edited my answer and added further explanations $\endgroup$ Jul 30 '13 at 21:10
  • $\begingroup$ @JasonGross, this question was answered in more detail before (see Mike's answer and my explanation): mathoverflow.net/questions/164343/… $\endgroup$ Aug 19 '14 at 17:03

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.