P

Paths in HITs

Describing paths in Higher Inductive Types (coequalizers and pushouts).