Conference item icon

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


Access Document


Files:
Publisher copy:
10.1109/LICS.2017.8005147

Authors


More by this author
Institution:
University of Oxford
Division:
MPLS
Department:
Computer Science
Role:
Author
More by this author
Institution:
University of Oxford
Oxford college:
Wadham College
Role:
Author
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
Source identifiers:
687059
ISBN:
9781509030187
Pubs id:
pubs:687059
UUID:
uuid:384f994d-f47f-4cc5-9a1e-bcd48612a336
Local pid:
pubs:687059
Deposit date:
2017-03-24

Terms of use


Views and Downloads






If you are the owner of this record, you can report an update to it here: Report update to this record

TO TOP