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 [Reedy model structures on oplax limits](https://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 [Reedy model structures on oplax limits](https://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?)



Explicit description of the oplax limit of a functor to Cat?
**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 ...


