Path Spaces of Higher Inductive Types in Homotopy Type Theory

Nicolai Kraus, Jakob von Raumer

The study of equality types is central to homotopy type theory. Characterizing these types is often tricky, and various strategies, such as the encode-decode method, have been deve…