Generalizing this definition, if $C$ is a non-small but accessible$(\infty,1)$-category with finite limits, we write

$Pro(C) := AccLex(C,\infty Grpd)^{op}
\,.$

for the category of left exact functors $C\to \infty Gprd$ which are moreover accessible. More generally, if $C$ is just locally small, then one can take $Pro(C)$ to be the infinity-category of small functors whose Grothendieck construction is cofiltered?. Equivalently, $Pro(C)$ consists of the functors which are “small cofiltered limits of representables”.