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
transpdoesn't compute on them.
- The nighly version of Agda currently displays a warning about not being able to generate equivalences. But Agda 18.104.22.168 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?