Constructions with non-recursive higher inductive types
Higher inductive types (HITs) in homotopy type theory are a powerful generalization of inductive types. Not only can they have ordinary constructors to define elements, but also higher constructors to define equalities (paths). We say that a HIT H is non-recursive if its constructors do not quantify...
| Main Author: | |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
2016
|
| Subjects: | |
| Online Access: | https://eprints.nottingham.ac.uk/33025/ |