Quotient inductive-inductive types
Higher inductive types (HITs) in Homotopy Type Theory (HoTT) allow the definition of datatypes which have constructors for equalities over the defined type. HITs generalise quotient types and allow to define types which are not sets in the sense of HoTT (i.e. do not satisfy uniqueness of equality pr...
| Main Authors: | , , , |
|---|---|
| Format: | Conference or Workshop Item |
| Published: |
2017
|
| Online Access: | https://eprints.nottingham.ac.uk/51210/ |