Questions tagged [inductive-family]

To discuss questions concerning inductive families. For example, the type of vectors of dimension N can be defined as an inductive family over the natural numbers.

Filter by
Sorted by
Tagged with
9 votes
1 answer

Current status of cubical inductive families

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 (...
Trebor's user avatar
  • 3,490