|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|
A homotopy -type is a space where we consider its properties with regard to the fundamental groups of its components.
A continuous map is a homotopy -equivalence if it induces isomorphisms on and 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. 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 will be a -groupoid).
See the general discussion in homotopy n-type.
A connected pointed homotopy 1-type is completely determined, up to (weak) homotopy equivalence, by the one group . A connected homotopy 1-type with is an Eilenberg-Mac Lane space and is often written . A general homotopy 1-type can then be written as a disjoint union of such s, and is completely determined by its fundamental groupoid.
In the other direction, for any (discrete) group one can construct its classifying space , which is a . In fact, many versions of this construction (such as the geometric realization of the simplicial nerve ; see Dold-Kan correspondence) apply just as well to any groupoid. We can obtain any 1-type in this way, since a groupoid is up to homotopy type (of groupoids!) a disjoint union of groups. However this description is not natural in the category of groupoids, and is analogous to choosing a basis for a vector space.
Moreover, every continuous map between s is induced by a group homomorphism, every map between 1-types is induced by a functor between groupoids, and every homotopy is induced by a conjugation (aka a natural transformation between groupoids). In fact, one can show that the -category of homotopy 1-types is equivalent to the 2-category Grpd of groupoids, via the above-described correspondence..
There are further aspects to this relationship; for instance, the van Kampen theorem for the fundamental groupoid shows how the algebra of groupoids models the gluing of spaces. The general result for non-connected spaces is possible because groupoids model homotopy 1-types, having structure in dimensions 0 and 1. For the search for algebraic structures that play an analogous role to groupoids for -types with , see the pages homotopy hypothesis, fundamental infinity-groupoid, cat-n-group, classifying space, crossed complex, and probably others.
|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|