Homotopy Type Theory homotopy level > history (changes)

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

~~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~~

~~$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)~~

Last revised on June 15, 2022 at 22:39:51. See the history of this page for a list of all contributions to it.