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.
2
questions
2
votes
1
answer
195
views
Which would be better for programming using Homotopy type theory Agda or Idris
I'm looking to model data inputs for an artificially intelligent system, which is affected by its internal parts and has feedback loops. I'd like to model it mathematically, using category theory or ...
- 21
7
votes
1
answer
427
views
What should we return when pattern matching on a Path constructor?
Context: Cubical Type Theory
Consider a simple HIT, say, an HitInt:
...
- 888