# Homotopy Type Theory Whitehead's principle > history (Rev #1)

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