|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|
The notion of homotopy -type is a coarsened variant of the notion of homotopy type, that latter notion being recovered for .
Among the most important invariants of a topological space or, more generally, of an object in an ∞-stack (∞,1)-topos are its homotopy groups . We say that an object for which all with are trivial is a homotopy -type. More precisely, these are the n-truncated objects and one says that two object , are of the same homotopy -type if there is a zig-zag of morphisms connecting them that induces isomorphisms on homotopy groups for .
Homotopy -types are, thus, the equivalence classes of an equivalence relation imposed on objects in Top (or objects in another (∞,1)-topos). Thus, we often say, roughly, that two spaces ‘have the same homotopy -type’ if their homotopy groups agree up to , and ‘a homotopy -type’ can equally well be represented by any space having that -type. This is analogous to the definition of ‘a real number’ as an equivalence class of Cauchy sequences. However, as usual in homotopy theory, merely having isomorphic homotopy groups is not enough; rather there needs to be a map inducing such an isomorphism. Thus, the relevant equivalence relation relates two spaces when there is a zigzag of maps between them, all inducing isomorphisms on homotopy groups for . One can then show that any space is equivalent, in this sense, to one having trivial homotopy groups above level , so that the other definition is also correct.
The use of topological spaces is not, of course, essential; we could just as well use any other structure that models the same homotopy theory, such as simplicial sets, simplicial groupoids, or (for connected spaces) simplicial groups. Moreover, the fact that homotopy -types can be modeled by spaces that are ‘homotopically trivial’ above level raises the possibility of finding reasonably complete algebraic models for such -types.
A continuous map is a homotopy -equivalence if it induces isomorphisms on for at each basepoint. Two spaces share the same homotopy -type if they are linked by a zig-zag chain of homotopy -equivalences.
For any space , you can kill its homotopy groups in higher dimensions by attaching cells, thus constructing a new space so that the inclusion of into is a homotopy -equivalence; up to (weak) homotopy equivalence, the result is the same for any space with the same homotopy -type as . Accordingly, a homotopy -type may alternatively be defined as a space with trivial for , or as the unique (weak) homotopy type of such a space, or as its fundamental -groupoid (which should be an -groupoid, by one direction of the homotopy hypothesis).
One can also construct model structures on whose homotopy categories are the categories . This is one of the original examples of Bousfield localization. From this perspective, the above replacement of a space by one having trivial for is an example of fibrant replacement.
We will use simplicial groups and simplicial groupoids rather than spaces below as they are already partially algebraicised. So in the definition above, ‘space’ means a simplicial group(oid) and ‘continuous map’ means a homomorphism of simplicial group(oid)s.
Considerable effort has gone into finding ‘good’ algebraic models for (connected) homotopy -types. In low dimensions the results are ‘old’ or ‘classical’. We will consider connected cases (simplicial groups) only. The extension to the non-connected case (simplicial groupoids) is ‘routine’.
The 1-type of a connected space is completely determined by its fundamental group, so groups form an algebraic model for homotopy 1-types. For the non pointed case, we can say groupoids form an algebraic model.
S. Mac Lane and J. H. C. Whitehead, On the 3-type of a complex, Proc. Nat. Acad. Sci. U.S.A., 36, (1950), 41 – 48.
Finding the algebraic model for the -types is just a start. Ideally one searches for algebraic models of all the higher homotopy structure as well. This was done by Jean-Louis Loday using the notion of a cat-n-group.
The method initiated by J.H.C. Whitehead was to approximate homotopy theory by models which analysed particular types of behaviour. One of his most widely followed models is that of stable homotopy theory. The opposite method was to find algebraic models of restricted classes of spaces, such as 2-types, or with cells in a small range of dimensions. H.-J. Baues has followed up many of the latter ideas.
It is sensible to regard crossed complexes as giving a linear model of homotopy types. These crossed complexes are equivalent to strict globular -groupoids. Although these are restricted model of homotopy types, they are convenient in many aspects, because of the many analogies with the familiar chain complexes.
Crossed complexes capture operations of the fundamental groupoid, but not quadratic information such as Whitehead products (for dimensions ). However one can define -fold crossed complexes inductively as crossed complexes internal to -fold crossed complexes. So one can give the
(Conjecture) double crossed complexes capture the quadratic information on homotopy types, triple crossed complexes capture the cubic information, etc., etc.
This has the possibility of leading to computations, by applying van Kampen theorems to specific levels.
|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|