Abstract: Higher inductive types are a generalization of inductive types. While an inductive type is generated by certain terms, a higher inductive type may be generated by terms, paths between terms, paths between paths between terms, etc. In the homotopy theoretic model of type theory, this corresponds to constructing cell complexes. We will see many other uses of higher inductive types, and will sketch the argument that $\pi_1(S^1)$ is isomorphic to the integers.