Overview

One key attraction of HoTT (homotopy type theory) is for doing homotopy theory synthetically - like how one does Euclidean geometry from axioms without needing the existence of the real numbers. In this arc we will formalize what it means for the circle S¹ to have fundamental group ℤ in this setting.

Applying the philosophy of trinitarianism, is strongly recommended in this arc. However, it is designed so that anyone eager to see familiar geometric results can also start here with no prerequisites. Hence, this arc mostly adopts a geometric (hence categorical) perspective on types.