nLab
complete small category

Complete small categories

Context

Category theory

Limits and colimits

Complete small categories

Definition

A complete small category (or small complete category) is a category which is both small (has only a set of objects and morphisms) and complete (has a limit of every small diagram).

(Note that the phrase “small-complete category” is sometimes used to mean merely a complete category, i.e. one which is “complete relative to small diagrams”. Therefore, “complete small category” is a safer term for our concept.)

In classical logic

In the presence of classical logic, complete small categories reduce to complete lattices by the following theorem of Freyd.

Theorem

If (in some universe UU) a small category DD has products of families of objects whose size is at least that of its set of morphisms, then DD is a preorder. In particular, any complete small category is a preorder.

Proof

Let xx, yy be any two objects, and suppose (contrary to DD being a preorder) that there are at least two different morphisms xsryx \,\underoverset{s}{r}{\rightrightarrows}\, y. Then the set of morphisms

x fMor(D)yx \to \prod_{f \in Mor(D)} y

has cardinality at least 2 |Mor(D)|>|Mor(D)|2^{|Mor(D)|} \gt {|Mor(D)|}, which is a contradiction.

In Grothendieck toposes

The internal logic of a topos is not, in general, classical, so the above proof does not apply when considering internal categories in a topos. However, in a Grothendieck topos, one can show that the conclusion still holds by essentially reducing the question to the analogous one in SetSet. A brief description of the argument can be found in the answer to this question.

In more general toposes and constructive mathematics

However, it is possible to have non-preorder complete small categories in non-Grothendieck topoi. In particular, the effective topos, along with most other realizability toposes, does contain such internal categories.

It follows that, in constructive mathematics, it is impossible to prove even that every complete small category in SetSet or in a Grothendieck topos must be a preorder.

Modelling impredicative type theory

Complete small categories have applications to the modeling of impredicative polymorphism. Suppose that there is a full subcategory C\mathbf C of Set\mathbf{Set} that is small and complete. (This postulate is consistent with intuitionistic set theory, as shown by the realizability models mentioned above.) Then we can interpret an impredicatively-quantified type as

X.T= ACT A/X\⟦ \forall X.T \⟧ = \prod_{A\in \mathbf{C}} \⟦ T\⟧_{A/X}

although there are more elaborate formulations that use a subset of this product.

More precisely, if we ask for an actually small complete category of sets then the notion of completeness has to be defined carefully. An alternative approach is to suppose that there is a full replete subcategory 𝒞\mathcal{C} of Set\mathbf{Set} which is complete in the sense of being closed under set-indexed products and equalizers, yet essentially small, i.e. with a small skeleton C\mathbf C. (Being replete, 𝒞\mathcal{C} will not itself be small.)

References

  • A small complete category, Martin Hyland, Annals of Pure and Applied Logic 40 (1988), pdf

There was much activity around that time, by Peter Freyd, Eugenio Moggi, Andrew Pitts, John Reynolds, Guiseppe Rosolini, and others.

For a more recent treatment, the idea of using a replete complete subcategory which is essentially small in IZF is discussed in

  • Relational parametricity for computational effects, Rasmus Møgelberg and Alex Simpson, Logical Methods in Computer Science, Vol 5 (3:7), 2009. arxiv.

Last revised on December 7, 2018 at 07:50:52. See the history of this page for a list of all contributions to it.