## Definition ## Whitehead's principle says that given types $A$ and $B$ and function $f:A \to B$, if the set-truncation of $f$ is an [[equivalence]] and the $n$-th homotopy group of $f$ is an equivalence, then $f$ is an equivalence. $$\frac{A\ \mathrm{type} \quad B\ \mathrm{type} \quad f:A \to B \quad p:\mathrm{isEquiv}(\left[f\right]_0) \quad q:\prod_{n:\mathbb{N}} \mathrm{isEquiv}(\pi^n(f))}{r:\mathrm{isEquiv}(f)}$$ ### In universes ### Whitehead's principle is said to hold in a [[universe]] $\mathcal{U}$ if the universe comes with a dependent function $$p:\prod_{A:\mathcal{U}} \prod_{B:\mathcal{U}} \prod_{f:\mathcal{T}_\mathcal{U}(A) \to \mathcal{T}_\mathcal{U}(B)} \left(\mathrm{isEquiv}(\left[f\right]_0) \times \prod_{n:\mathbb{N}} \mathrm{isEquiv}(\pi^n(f))\right) \to \mathrm{isEquiv}(f)$$ ## See also ## * [[limited principle of omniscience]] * [[excluded middle]] * [[double negation]]