On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory