nLab complete small category

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 due to Freyd 64, p. 78. .

Theorem

If a category $D$ has products of families of objects whose size is at least that of its set of morphisms, then $D$ is a preorder. In particular, any complete small category is a preorder.

Proof

Let $x$, $y$ be any two objects, and suppose (contrary to $D$ being a preorder) that there are at least two different morphisms $x \rightrightarrows y$. Then the set of morphisms

$$D(x, \prod_{f \in Mor(D)} y) \cong \prod_{f \in Mor(D)} D(x, y)$$

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

This basic fact has profound implications for instance for the adjoint functor theorem and the existence of Kan extensions. See there for more.

(More generally, we only need to assume the existence of powers, not arbitrary products.)

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 Set. 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, arising for example from the modest sets or partial equivalence relations. See Hyland88 and HRR90 for details.

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

There is a subtlety, however, because in the absence of the axiom of choice, there is a difference between a category being “strongly complete” in the sense of being equipped with limit-assigning functors, and being “weakly complete” in the sense that there merely exists a limit for every diagram. The complete small categories in realizability toposes are only weakly complete, which categorically means that only the stack completions of their corresponding indexed categories are complete in the relevant indexed-category sense.

It seems to be unknown whether there exists a (necessarily non-Grothendieck) topos containing a strongly complete small category. However, one of the complete small categories in the effective topos does become strongly complete when the ambient context is restricted to the subcategory of assemblies rather than the entire effective topos.

Modelling impredicative type theory

Complete small categories have applications to the modeling of impredicative polymorphism. Suppose that there is a full subcategory $\mathbf C$ of $\mathbf{Set}$ that is small and complete. Then we can interpret an impredicatively-quantified type as

$$\llbracket \forall X.T \rrbracket = \prod_{A\in \mathbf{C}} \llbracket T\rrbracket_{A/X}$$

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

At least at first glance, this requires $\mathbf{C}$ to be strongly complete. Hence it works in the category of assemblies, but not the entire realizability topos.

An alternative approach is to suppose that there is a full replete subcategory $\mathcal{C}$ of $\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 $\mathbf C$. (Being replete, $\mathcal{C}$ will not itself be small.) Such a category can be obtained as the repletion of any weakly complete actually small subcategory, such as exist in realizability toposes. See RS04 and MS09. The interpretation of the impredicative $\forall$ is then achieved by a product over the sets in the small skeleton $\mathbf C$. However, to eliminate terms of type $\forall$, one must pick an isomorphism to a set in the skeleton, and be confident that the choice does not matter, and for this reason a relational parametricity is built in to the interpretation of $\forall$. In more detail:

$$\llbracket \forall X.T \rrbracket = \{\pi\in \prod_{A\in \mathbf{C}} \llbracket T\rrbracket_{A/X} | \forall R\subseteq A\times B. \mathcal{R}_R( \pi(A),\pi(B))\}$$

where $\mathcal{R}_R$ is a binary logical relation, suitably defined, and

$$\llbracket (t:\forall X.T)(U)\rrbracket = gpd(i)(\llbracket t\rrbracket_D)$$

where $i\colon D \to \llbracket U\rrbracket$ is a bijection with a set in the skeleton $\mathbf C$, and we are using the fact that for any bijection $j\colon C\to D$, there is a functorial action $gpd(j)\llbracket T\rrbracket_{C/X}\to \llbracket T\rrbracket_{D/X}.$ For discussion about whether this works, see the nForum thread for this page.

Note that to model polymorphic simple type theory such as System F, it is not necessary for this purpose that $\mathbf{C}$ be complete; all it needs is to have products indexed by its own set of objects. Freyd’s theorem does not apply in this case, since there might be fewer objects than morphisms; and indeed there are plenty of categories even classically that have products indexed by their set of objects, e.g. any one-object category. It is true, however, that (assuming classical logic) no full subcategory of $Set$ can have products indexed by its own set of objects; this (and a bit more) was shown in Reynolds 84, again by reducing to Cantor’s diagonal argument. On the other hand, to break this argument we do not have to move to realizability; Grothendieck toposes suffice, as shown in Pitts 87 via the Yoneda embedding of a syntactic model into its topos of presheaves.

In contrast, something more like a true complete small category may be necessary to model an impredicative dependent type theory such as the calculus of constructions with a proof-relevant impredicative sort (traditionally called “Set”), where the impredicative universe admits Pi-types with arbitrary domain.

Related concepts

• adjoint functor theorem

References

Theorem appears as exercise D in ch.3 (p.78) in:

• Peter Freyd, Abelian Categories, Harper & Row New York 1964. (Reprinted with author’s comment as TAC reprints no. 3 (2003))

Reviewed as Thm. 2.1 in:

• Michael Shulman, Set theory for category theory (arXiv:0810.1279)

The original reference for the complete small categories in the effective topos is:

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

It was expanded further in the following paper, which discusses the strong/weak completeness issue and the relation to stacks in more detail:

• Hyland, J. M., Robinson, E. P. and Rosolini, G. (1990), The Discrete Objects in the Effective Topos. Proceedings of the London Mathematical Society, s3-60: 1-36. doi:10.1112/plms/s3-60.1.1

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

• John Reynolds, Polymorphism is not set-theoretic. In: Kahn G., MacQueen D.B., Plotkin G. (eds) Semantics of Data Types. SDT 1984. Lecture Notes in Computer Science, vol 173. Springer, Berlin, Heidelberg

• Andy Pitts, Polymorphism is Set Theoretic, Constructively. In Category Theory and Computer Science, Proceedings, Edinburgh 1987, Lecture Notes in Computer Science Vol. 283 (Springer-Verlag, Berlin, 1987), pp 12-39, PDF

A more recent survey of this type of model for polymorphic type theory is in

• Andrea Asperti and Simone Martini, Categorical models of polymorphism, Information and Computation, Volume 99, Issue 1, 1992, Pages 1-79, DOI90024-A.)

The idea of using a replete complete subcategory which is essentially small in IZF is discussed in

• Using Synthetic Domain Theory to Prove Operational Properties of a Polymorphic Programming Language Based on Strictness“, Guiseppe Rosolini and Alex Simpson, unpublished, 2004. ResearchGate

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

The interplay with colimits is discussed in

• Duško Pavlović, On completeness and cocompleteness in and around small categories , APAL 74 (1995) pp.121-152.