In this work we introduce some basic concepts within homotopy type theory (HoTT), a proposed alternative mathematical foundation to classical set theory. In particular, our discussion revolves around the Axiom of Choice (AC). In Part I, we introduce the classical AC and some of its most important equivalents. In Part...