categories: Re: Pro C

[rosicky@math.muni.cz (Jiri Rosicky)]

< Choice isn't needed: all you need is the result that, for any filtered
< category C, there is a directed poset P and a final functor P --> C.
< There is a proof of this somewhere in SGA4 (I don't have the reference
< to hand), where it is attributed to Pierre Deligne; but I suspect it
< may be older than this.

< Peter Johnstone

The proof is also in my book with Adamek, Locally presentable and accessible
categories, Theorem 1.5,
Jiri Rosicky