Explicit description of the oplax limit of a functor to Cat?

Question

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?)

Answer 1

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.

[edit]

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 ...