Would the following (aside from the first) help to prepare a more digestible proof of Barr's full regular embedding theorem? 1) Say that an object U of a (but not just any) category E is open if U is a finitely presentable object of the opposite of E (i.e., if it satisfies the analogue of the filter convergence characterization of open sets). An object P of E is strict if it is the projective limit of a diagram of opens such that each limit projection is an effective epimorphism; P is called saturated if for every U -->> V of opens, each P -->> V lifts to some P -->> U; finally, P is called weakly projective if it is projective with respect to effective epimorphisms of opens. Every strict, saturated object is weakly projective. 2) Given P in Pro(C), where C is a regular category, let P' denote the fibred product of all X -->> P which are opens of Pro(C)/P, and P* the projective limit of: P <<-- P' <<-- P'' <<-- P''' ...; one shows that the projection P* --> P is an effective epimoprhism, that P* is a strict, saturated object of Pro(C)/P, and therefore that P* is a weakly projective object of Pro(C). Theorem 14 of Barr's '86 JPAA paper (i.e., step three in his message of 21 May) applies. 3) The construction is (to my knowledge) due to Joyal (c. 1972, or earlier). Objects of the form X*, where X is an object of C, are principal prime models, a notion Makkai (Full continuous embeddings of toposes, Trans AMS, 1982) distilled from Barr's original proof (Joyal called them absolutely flasque). cheers, -b PS:Without the terminology, that Pro(C) (=~ Lex(C,Set)^op) is regular if C is is suggested in SGA4, Expose I, 8.9 (especially cf. exercise 8.9.9(b)).