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.
1
question
9
votes
1
answer
369
views
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 (...
- 376