Path Spaces of Higher Inductive Types in Homotopy Type Theory