Higher inductive types are a useful concept in homotopy type theory. However, considering its general syntax is a bit of a challenge. Is it possible to implement all higher inductive types with just generalized algebraic data types and non-truncated quotients?
Construct higher inductive types with only generalized algebraic data types and non-truncated quotients?
Hexirp
- 325
- 2
- 10