Homotopy Type Theory
Whitehead's principle > history (changes)
Showing changes from revision #1 to #2:
Added | Removed | Changed
Definition
< Whitehead's principle
Whitehead’s principle says that given types and and function , if the set-truncation of is an equivalence and the -th homotopy group of is an equivalence, then is an equivalence.
In universes
Whitehead’s principle is said to hold in a universe if the universe comes with a dependent function
See also
Last revised on June 14, 2022 at 04:43:28.
See the history of this page for a list of all contributions to it.