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