## Definition ## A type $A$ has a __homotopy level__ or __h-level__ of $n$ if the type $hasHLevel(n, A)$ is inhabited, for [[natural numbers|natural number]] $n:\mathbb{N}$. $hasHLevel(n, A)$ is inductively defined $$hasHLevel(0, A) \coloneqq isContr(A)$$ $$hasHLevel(s(n), A) \coloneqq \prod_{a:A} \prod_{b:A} hasHLevel(n, a =_A b)$$ ## Examples ## * Every [[proposition]] has a homotopy level of $1$. * Every [[set]] has a homotopy level of $2$. ## See also ## * [[truncation]] * [[inhabited type]] * [[monic function]] * [[epic function]] ## Referencees ## * Ayberk Tosun, Formal Topology in Univalent Foundations, ([pdf](https://odr.chalmers.se/handle/20.500.12380/301098))