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.