Current status of cubical inductive families

Question

I have the impression that cubical type theory hasn't dealt with inductive families yet. But the only source on this matter I can get is this Agda issue. What I've gathered is

• Agda supports defining (higher) inductive families, but transp doesn't compute on them.
• The nighly version of Agda currently displays a warning about not being able to generate equivalences. But Agda 2.6.2.2 doesn't even display this warning.
• The other cubical proof assistants I inverstigated don't seem to support inductive families.

What's the status on this matter? In particular,

• Is there a conjectured (complete or partial) set of rules in this situation?
• If so, is there any theoretical analysis (consistency, canonicity, normalization) of these rules?
• To what extent have the rules been implemented in any cubical proof assistant?

Answer 1

I would take a look at Higher inductive types in cubical computational type theory by Evan Cavallo and Bob Harper.

This paper provides:

• A complete set of rules for the formation and computation of higher inductive families
• A canonicity result

Fair warning that the rules are pretty brutal and difficult to read, and I make no claim to understand them myself.

It uses Cartesian cubical type theory, instead of the DeMorgan cubical type theory implemented in Agda, so there is no mention of transp. The closest thing is coe, which allows coercion between arbitrary dimension variables along a line of types.

To my knowledge, this paper has never been implemented in its entirety in a cubical proof assistant. redtt implements the non-indexed fragment.