The HoTT Perspective: Inductive Types up to Path Equivalence

We give a self-contained development of Homotopy Type Theory as the synthetic language in which natural numbers admit an encoding-free description. The natural numbers are the inductive type N generated by zero and succ; identity types carry the homotopical content of path spaces. We state Voevodsky's univalence axiom (A = B) ≃ (A ≃ B) and prove its fundamental consequence: the type Σ(X:U)(X ≃ N) of "structures equivalent to N" is contractible.