# Contents

## Idea

The term homotopy level (or h-level), originating in homotopy type theory, is another name for the notion of truncation (particularly in (∞,1)-categories and their internal language of homotopy type theory) in which the numbering is offset by 2:

a homotopy n-type is a type of homotopy level $n+2$.

This offset in counting enables it to “start” at 0 rather than (-2), which is convenient when defining it by induction over the natural numbers in type theory. Thus, the correspondence between the various terminologies is indicated in the following table.

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 valuemere proposition, h-proposition
h-level 20-truncateddiscrete space0-groupoid/setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/groupoid(2,1)-sheaf/stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoidh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoidh-3-groupoid
h-level $n+2$$n$-truncatedhomotopy n-typen-groupoidh-$n$-groupoid
h-level $\infty$untruncatedhomotopy type∞-groupoid(∞,1)-sheaf/∞-stackh-$\infty$-groupoid

Revised on March 9, 2014 23:28:22 by Urs Schreiber (89.204.139.55)