generalized the




In natural language, the definite article (‘the’ in English) is generally used only for nouns which are uniquely characterized by context. Hence we have “the United States of America” and “the book I was just reading,” but only “a car” or “a wild late-night party.” (Sometimes “the book I was just reading” is abbreviated to “the book”, but it should be clear from context that only one book could be meant.) Philosophers call this use of the definite article to pick out an individual definite description.

In mathematics, and especially in category theory, homotopy theory and higher category theory, it is common to use “the” more generally for something which is characterized uniquely up to unique coherent isomorphism (that is, a unique isomorphism appropriate given the context).

Thus, for instance, we speak (assuming that any exists) of “the” terminal object of a category, “the” product of two objects, “the” left adjoint of a functor, and so on. Outside of pure category theory we have examples such as “the” Dedekind-complete ordered field (the field of real numbers).

In higher category theory, we extend this usage to objects that are characterized uniquely up to unique coherent equivalence. Of course, by “unique equivalence” we mean “unique up to 2-equivalence,” and so on. A more homotopy-theoretic way to say this is that the space (\infty-groupoid) of all such objects is contractible.


The notion of a “generalized the” can be formalized and treated uniformly in homotopy type theory. Here one can define an introduction rule for the as follows:

(A:Type),((a,p):IsContr(A))(the(A,a,p):A). (A:Type),((a,p):IsContr(A)) \vdash (the(A,a,p):A).

Here the term (a,p)(a,p) is one witness for the contractibility of the type AA. Then we have the(A,a,p)=a:Athe(A,a,p)=a:A.

Since IsContr(A)IsContr(A) is itself contractible, we could say that (a,p)(a,p) is the witness for the contractibility of the type AA, which may explain why we do not generally mention it.

If we wish to extend this treatment to types which are propositions, we might call such types FactThat(P)FactThat(P), for some statement PP. Then if PP holds, we can introduce a term the(FactThat(P))the(FactThat(P)).


  • David Corfield, Expressing ‘The Structure of’ in Homotopy Type Theory, pdf, revised as Chapter 4 of Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy.

Last revised on August 10, 2020 at 10:30:01. See the history of this page for a list of all contributions to it.