Higher Inductive Type Eliminators Without Paths

Higher Inductive Type Eliminators Without Paths
Nils Anders Danielsson
25th International Conference on Types for Proofs and Programs, TYPES 2019 (10.4230/LIPIcs.TYPES.2019.10). [pdf, highlighted Agda code, zip file with code]

Abstract

Cubical Agda has support for higher inductive types. Paths are integral to the working of this feature. However, there are other notions of equality. For instance, Cubical Agda comes with an identity type family for which the J rule computes in the usual way when applied to the canonical proof of reflexivity, whereas typical implementations of the J rule for paths do not.

This text shows how one can use some of the higher inductive types definable in Cubical Agda with arbitrary notions of equality satisfying certain axioms. The method works for several examples taken from the HoTT book, including the interval, the circle, suspensions, pushouts, the propositional truncation, a general truncation operator, and set quotients.