homotopy 1-type


Homotopy theory

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




A homotopy 11-type is a space where we consider its properties with regard to the fundamental groups π 1\pi_1 of its components.


A continuous map XYX \to Y is a homotopy 11-equivalence if it induces isomorphisms on π 0\pi_0 and π 1\pi_1 at each basepoint. Two spaces share the same homotopy 11-type if they are linked by a zig-zag chain of homotopy 11-equivalences.

For any space XX, you can kill its homotopy groups in higher dimensions by attaching cells, thus constructing a new space YY so that the inclusion of XX into YY is a homotopy 11-equivalence; up to (weak) homotopy equivalence, the result is the same for any space with the same homotopy 11-type. Accordingly, a homotopy 11-type may alternatively be defined as a space with trivial π i\pi_i for i>1i \gt 1, or as the unique (weak) homotopy type of such a space, or as its fundamental \infty-groupoid (which will be a 11-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 π 1\pi_1. A connected homotopy 1-type with π 1=G\pi_1 = G is an Eilenberg-Mac Lane space and is often written K(G,1)K(G,1). A general homotopy 1-type can then be written as a disjoint union of such K(G,1)K(G,1)s, and is completely determined by its fundamental groupoid.

In the other direction, for any (discrete) group GG one can construct its classifying space G\mathcal{B}G, which is a K(G,1)K(G,1). In fact, many versions of this construction (such as the geometric realization of the simplicial nerve nerve(G)nerve(G); 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 K(G,1)K(G,1)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 (,1)(\infty,1)-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 nn-types with n>1n\gt 1, see the pages homotopy hypothesis, fundamental infinity-groupoid, cat-n-group, classifying space, crossed complex, and probably others.

homotopy leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/unit type/contractible type
h-level 1(-1)-truncated(-1)-groupoid/truth value(0,1)-sheafmere proposition, h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/groupoid(2,1)-sheaf/stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheafh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheafh-3-groupoid
h-level n+2n+2nn-truncatedhomotopy n-typen-groupoid(n+1,1)-sheafh-nn-groupoid
h-level \inftyuntruncatedhomotopy type∞-groupoid(∞,1)-sheaf/∞-stackh-\infty-groupoid

Revised on February 18, 2015 19:03:10 by Urs Schreiber (