Data structures for quasistrict higher categories

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Authors

Colleges, School and Institutes

External organisations

  • University of Oxford

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 approaches, and gives a practical method for performing calculations in quasistrict 4-categories. 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.

Details

Original languageEnglish
Title of host publicationProceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Publication statusPublished - 18 Aug 2017
Event32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) - Reykjavik, Iceland
Duration: 20 Jun 201723 Jun 2017

Conference

Conference32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
CountryIceland
CityReykjavik
Period20/06/1723/06/17