Changed indPath definitions to reflect migration to HoTT-Agda library.