There are some answers to this way back. There is a lovely answer to several of your questions in
D. A. Edwards and H. M. Hastings, 1976, ˇCech and Steenrod homotopy theories with applications to geometric topology , volume 542 of Lecture Notes in Maths , Springer-Verlag.
The category of prosimplicial sets has a model category structure that corresponds to a geometrically defined notion of strong shape theory (i.e. a homotopy coherent version of Borsuk's shape theory). Edwards and hastings Hastings extended a result of Chapman and showed this model category theory also to be a form of proper homotopy theory. (There is also some discussion of this in my article:
T. Porter, 1995, Proper homotopy theory , in Handbook of Algebraic Topology , 127–167, North-Holland, Amsterdam. )
The story does not end there. Because of the connection with étale homotopy theory (Artin and Mazur), there was a revival of interest in procateories pro-categories in the last few years and there is a good discussion in
H. Fausk and D. Isaksen, Model structures on pro-categories , Homology, Homotopy and Applications, 9, (2007), 367 – 398.
I suggest that you also look at others of Dan Isaksen's papers on this area as they answer more of the quetions that you have asked.
On another point that you mention, the rectification process for properties is reasonably well understood due to what is known as the reindexing lemma (the simplest case is in Artin and Mazur's lecture notes but there are much fuller versions some of which are discussed in another of Isaksen's papers
D. C. Isaksen, Completions of pro-spaces , Math. Z., 250, (2005), 113 – 143. )
If you read these papers carefully you will come to the conclusion that certain problems are still not fully understood especially when pro-finite simplicial sets are concerned, and the applications of those beasties are again very important so that is a good area to explore!!!
(See also work by Quick (Profinite homotopy theory , Documenta Mathematica, 13, (2008), 585–612.) and Pridham (Pro-algebraic homotopy types , Proc. Lond. Math. Soc. (3), 97, (2008), 273 – 338. ) They show some of the more recent stuff on this with some good applications. There are copies on the ArXiv.)
