homotopy theory, (∞,1)-category theory, homotopy type theory
flavors: stable, equivariant, rational, p-adic, proper, geometric, cohesive, directed…
models: topological, simplicial, localic, …
see also algebraic topology
Introductions
Definitions
Paths and cylinders
Homotopy groups
Basic facts
Theorems
homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
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 Moon” 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/homotopy type theory and generally in higher category theory, it is common to use “the” more generally for objects/types which are characterized only up to coherent isomorphism/equivalence: Such need not actually be unique, but any two of them are isomorphic or more generally coherently equivalent in an essentially unique way (meaning that the ∞-groupoid of all such objects is contractible).
For example, one speaks (assuming that any exists) of “the” terminal object of a category, “the” Cartesian 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).
The notion of a “generalized the” can be formalized and treated uniformly in homotopy type theory. Here one may define an introduction rule for the as follows:
Here the term is one witness for the contractibility of the type . Then we have .
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 ‘’.
The term “generalized the” was introduced by James Dolan and may first appear in print here:
Quoting:
Given a tensor product of the 2-Hilbert spaces and , we often write its underlying 2-Hilbert space as . This notation may tempt one to speak of ‘the’ tensor product of and , which is is legitimate if one uses the generalized ‘the’ as advocated by Dolan [7]. In a set, when we speak of ‘the’ element with a given property, we implicitly mean that this element is unique. In a category, when we speak of ‘the’ object with a given property, we merely mean that this object is unique up to isomorphism — typically a specified isomorphism. Similarly, in a 2-category, when we speak of ‘the’ object with a given property, we mean that this object is unique up to equivalence — typically an equivalence that is specified up to a specified isomorphism. This is the sense in which we may refer to ‘the’ tensor product of and . The generalized ‘the’ may be extended in an obvious recursive fashion to -categories.
Discussion in homotopy type theory:
Last revised on October 15, 2024 at 18:49:42. See the history of this page for a list of all contributions to it.