Data structures for quasistrict higher categories

Krzysztof  Bar; Jamie Vicary

doi:10.1109/LICS.2017.8005147

Data structures for quasistrict higher categories

Krzysztof Bar, Jamie Vicary

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

2 Citations (Scopus)

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.

Original language	English
Title of host publication	Proceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Publisher	IEEE Computer Society
Number of pages	12
ISBN (Print)	9781509030187
DOIs	https://doi.org/10.1109/LICS.2017.8005147
Publication status	Published - 18 Aug 2017
Event	32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) - Reykjavik, Iceland Duration: 20 Jun 2017 → 23 Jun 2017

Conference

Conference	32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)
Country/Territory	Iceland
City	Reykjavik
Period	20/06/17 → 23/06/17

Access to Document

10.1109/LICS.2017.8005147

Cite this

@inproceedings{f90b3c05be6b439297521a8e955dc85b,

title = "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 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.",

author = "Krzysztof Bar and Jamie Vicary",

year = "2017",

month = aug,

day = "18",

doi = "10.1109/LICS.2017.8005147",

language = "English",

isbn = "9781509030187",

booktitle = "Proceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)",

publisher = "IEEE Computer Society",

address = "United States",

note = "32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017) ; Conference date: 20-06-2017 Through 23-06-2017",

}

TY - GEN

T1 - Data structures for quasistrict higher categories

AU - Bar, Krzysztof

AU - Vicary, Jamie

PY - 2017/8/18

Y1 - 2017/8/18

N2 - 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.

AB - 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.

U2 - 10.1109/LICS.2017.8005147

DO - 10.1109/LICS.2017.8005147

M3 - Conference contribution

SN - 9781509030187

BT - Proceedings of 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)

PB - IEEE Computer Society

T2 - 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2017)

Y2 - 20 June 2017 through 23 June 2017

ER -

Data structures for quasistrict higher categories

Abstract

Conference

Access to Document

Fingerprint

Cite this