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.)
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 (-groupoid) of all such objects is contractible.
Here the term is one witness for the contractibility of the type . Since is itself contractible, we could say that is the witness for the contractibility of the type , 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 , for some statement . Then if holds, we can introduce a term .