Homotopy Type Theory homotopy level > history (Rev #2)

Definition

A type $A$ has a homotopy level or h-level of $n$ if the type $hasHLevel(n, A)$ is inhabited, for natural number $n:\mathbb{N}$. $hasHLevel(n, A)$ is inductively defined

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)