Path Spaces of Higher Inductive Types in Homotopy Type Theory
Path Spaces of Higher Inductive Types in Homotopy Type Theory
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 developed. We prove a theorem about equality types of coequalizers and pushouts, reminiscent of an induction principle and without any restrictions on the …