|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-proposition, mere proposition|
|cut rule||composition of classifying morphisms / pullback of display maps||substitution|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|logical conjunction||product||product type|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator, (idemponent) monad||modal type theory, monad (in computer science)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
|synthetic mathematics||domain specific embedded programming language|
Traditionally, a homotopy type is a topological space regarded up to weak homotopy equivalence, (although this may sometimes be referred to as its weak homotopy type, (see below)). Formally this may be taken to mean the object that represents in the standard homotopy category Ho(Top), or, better, in the (∞,1)-category ∞Grpd , the simplicial localization of the category Top at the weak homotopy equivalences, of which is the decategorification. As such, topological spaces regarded as homotopy types are equivalently ∞-groupoids (see at homotopy hypothesis for more on this).
More generally, then, we may think of every object in any (∞,1)-topos as being a homotopy type in the world of (just as we may think of an object of a 1-topos as being a “set in the world of ”). For instance, if is an (∞,1)-category of (∞,1)-sheaves/of ∞-stacks over some (∞,1)-site , then an object of may be thought of as a homotopy type over , or a sheaf of homotopy types. If is the classifying topos of some geometric theory , then an object of may be called a “-structured homotopy type”. And if is a cohesive (∞,1)-topos, an object of may be called a “cohesive homotopy type”. In the special case that , this reproduces the traditional notion.
The reason this makes sense is that any -topos has an internal language, which is homotopy type theory — a formal logic whose basic objects are abstract things called homotopy types, just as the basic objects of set theory are abstract things called sets. Inside the internal logic of , its objects behave like classical homotopy types (although the ambient logic is constructive). This explains why we can think of objects of as “homotopy types in the world of ”: they are the categorical semantics of these abstract homotopy types in the internal logic of . In the special case of , the internal and external logic are the same, so this meaning also includes the classical usage of “homotopy type”.
A homotopy type that is an n-truncated object in an (∞,1)-category or equivalently that interprets a type of homotopy level is also called a homotopy n-type or -type for short. For topological spaces / ∞-groupoids this means that all homotopy groups above degree a trivial.
In traditional homotopy theory of topological spaces one sometimes distinguishes the notion of strong homotopy types from that of weak homotopy types, depending on whether one regards topological spaces up to homotopy equivalence or up to weak homotopy equivalence (see also there the section Relation to homotopy types).
More precisely, weak homotopy equivalences between spaces give an equivalence relation on the class of topological spaces, and referring to a homotopy type means that you are to consider properties of a space that are shared by any of the spaces weakly equivalent to it and thus in that equivalence class. In this expanded sense, therefore, a homotopy type is such a weak equivalence class of spaces. Using the terminology from homotopy category, two spaces have the same homotopy type if they are isomorphic in Ho(Top).
By standard theorems, homotopy types in topological can also be ‘modeled’ by many other structures, such as
The sense of ‘modeled’ is related to Whithead’s algebraic homotopy theory. A setting such as those above acts as a model for homotopy types if there are comparison functors between and the category, and some notion of homotopy within the category yielding an equivalence of homotopy categories.
Although the notion of homotopy type is defined for arbitrary spaces, it is most usual to restrict attention to ‘locally nice’ spaces such as polyhedra (i.e. realisations of simplicial complexes or CW-complexes). Various other classes of space occur naturally in various parts of mathematics in particular in analysis and algebraic geometry and there the methods of abstract homotopy theory provide a way of mimicking the basic idea of homotopy type as described above.
Using variants of ‘weak equivalence’, for instance, ‘-equivalence’, one gets coarser notions of equivalence which can be very useful. The particular case of -equivalence leads to the related notion of homotopy n-type.
|homotopy level||n-truncation||homotopy theory||higher category theory||higher topos theory||homotopy type theory|
|h-level 0||(-2)-truncated||contractible space||(-2)-groupoid||true/unit type/contractible type|
|h-level 1||(-1)-truncated||contractible-if-inhabited||(-1)-groupoid/truth value||(0,1)-sheaf/ideal||mere proposition/h-proposition|
|h-level 2||0-truncated||homotopy 0-type||0-groupoid/set||sheaf||h-set|
|h-level 3||1-truncated||homotopy 1-type||1-groupoid/groupoid||(2,1)-sheaf/stack||h-groupoid|
|h-level 4||2-truncated||homotopy 2-type||2-groupoid||(3,1)-sheaf/2-stack||h-2-groupoid|
|h-level 5||3-truncated||homotopy 3-type||3-groupoid||(4,1)-sheaf/3-stack||h-3-groupoid|
There are some useful points made in: