Questions tagged [higher-inductive-types]
Higher inductive types (HITs) are a generalization of inductive types which allow the constructors to produce, not just points of the type being defined, but also elements of its iterated identity types.
1
question
6
votes
1answer
280 views
What should we return when pattern matching on a Higher Indutive Type and the case is a Path?
Context: Cubical Type Theory
Consider a simple HIT, say, an HitInt:
...
