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 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?
  • $\begingroup$ In univalent-math.github.io (ICMS 2020) there is a talk by Vezzosi about a construction (transpX) $\endgroup$
    – ice1000
    Apr 27, 2022 at 14:22

1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.