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.