The [nCatLab Grothendieck construction page](http://ncatlab.org/nlab/show/Grothendieck+construction#definition_10) 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 http://mathoverflow.net/questions/120382/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](http://ncatlab.org/nlab/show/dependent+sum) and [dependent product](http://ncatlab.org/nlab/show/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 http://mathoverflow.net/questions/120382/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?)