Conference item
Data structures for quasistrict higher categories
- Abstract:
- We present new data structures for quasistrict higher categories, in which associativity and unit laws hold strictly. Our approach has low axiomatic complexity compared to traditional algebraic definitions of higher categories, and we use it to give a practical definition of quasistrict 4-category. It is amenable to computer implementation, and we exploit this to give a machine-verified algebraic proof that every adjunction of 1-cells in a quasistrict 4-category can be promoted to a coherent adjunction satisfying the butterfly equations.
- Publication status:
- Published
- Peer review status:
- Peer reviewed
Actions
Authors
Bibliographic Details
- Publisher:
- IEEE Publisher's website
- Host title:
- 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- Publication date:
- 2017-08-18
- Acceptance date:
- 2017-03-22
- DOI:
- ISSN:
-
1043-6871
- ISBN:
- 9781509030187
Item Description
- Pubs id:
-
pubs:687059
- UUID:
-
uuid:384f994d-f47f-4cc5-9a1e-bcd48612a336
- Local pid:
- pubs:687059
- Source identifiers:
-
687059
- Deposit date:
- 2017-03-24
Terms of use
- Copyright holder:
- IEEE
- Copyright date:
- 2017
- Notes:
- Copyright © 2017 IEEE. This is the accepted manuscript version of the article. The final version is available online from IEEE at: https://doi.org/10.1109/LICS.2017.8005147
Metrics
If you are the owner of this record, you can report an update to it here: Report update to this record