The category of pro-objects of is written -. Such a category is sometimes called a ‘pro-category’, but notice that that is not the same thing as a pro-object in Cat.
“Pro” is short for “projective”. ( Projective limit is an older term for limit.) It is in contrast to “ind” in the dual notion of ind-object, standing for “inductive”, (and corresponding to inductive limit, the old term for colimit). In some (often older) sources, the term ‘projective system’ is used more or less synonymously for pro-object.
Cofiltered limits in Set are given by sets of threads and filtered colimits by germs (classes of equivalences), thus a representative of is a thread whose each component is a germ:
which can be more concretely written as ; thus where is some representative of the class; there is at least one for each ; if the domain is infinite, we seem to need an axiom of choice in general to find a function which will choose one representative in each class . Thus is given by the (equivalence class) of the following data
such that is a thread, i.e. for any we have an equality of classes (germs) . This equality holds if there is a and morphisms , such that . (Usually in fact people consider the dual of and the dual of as filtered domains). Now if we chose a different function instead then, , hence by the definition od classes, for every there is a and morphisms , such that .
Another, equivalent, definition is to let - be the full subcategory of the opposite functor category/presheaf category determined by those functors which are cofiltered limits of representables. This is reasonable since the copresheaf category is the free completion of , so - is the “free completion of under cofiltered limits.”
Procategories were used by Artin and Mazur in their work on étale homotopy theory. They associated to a scheme a ‘pro-homotopy type’. (This is discussed briefly at étale homotopy.) The important thing to note is that this was a pro-object in the homotopy category of simplicial sets, i.e., in the pro-homotopy category. Friedlander rigidified their construction to get an object in the pro-category of simplicial sets, and this opened the door to use of ‘homotopy pro-categories’.
The form of shape theory developed by Mardešić and Segal, at about the same time as the work in algebraic geometry, again used the pro-homotopy category. Strong shape, developed by Edwards and Hastings, Porter and also in further work by Mardešić and Segal, used various forms of rigidification to get to the pro-category of spaces, or of simplicial sets. There methods of model category theory could be used.
pro-object / pro-object in an (∞,1)-category
A. Grothendieck, Techniques de déscente et théorèmes d’existence en géométrie algébrique, II: le théorème d’existence en théorie formelle des modules, Seminaire Bourbaki 195, 1960, (pdf).
(SGA4-1) Théorie des topos et cohomologie étale des schémas. Tome 1: Théorie des topos, Séminaire de Géométrie Algébrique du Bois-Marie 1963–1964 (SGA 4). Dirigé par M. Artin, A. Grothendieck, et J. L. Verdier. Avec la collaboration de N. Bourbaki, P. Deligne et B. Saint-Donat. Lecture Notes in Mathematics 269, Springer 1972.
S. Mardešić, J. Segal, Shape theory, North Holland 1982