A small complete category (Q1112159): Difference between revisions

A well-known result of classical category theory asserts that a complete category which is small must be a preordered set. It was first observed by Eugenio Moggi (unpublished) that this result is not true constructively, in that the category \(\underset \tilde{} M\) of modest sets (in the sense of Dana Scott) forms a small full subcategory of the effective topos which is complete in a suitable sense. This paper presents a careful and detailed proof of Moggi's observation: the care is necessary (in defining the notions of small full subcategory and of completeness for such categories) because it is tempting to believe (as the author freely admits he did for a time) that \(\underset \tilde{} M\) satisfies a stronger form of completeness than it actually does. The paper ends with a brief discussion of the way in which \(\underset \tilde{} M\) may be used to construct models for strong type theories such as the polymorphic lambda calculus.