Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
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.