Showing changes from revision #0 to #1:
Added | Removed | Changed
Definition
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