A type theory for strictly unital infinity-categories
View / Open Files
Authors
Vicary, Jamie
Rice, Alex
Finster, Eric
Reutter, David
Publication Date
2022-08-04Journal Title
LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
Conference Name
Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
ISBN
9781450393515
Publisher
Association for Computing Machinery
Type
Conference Object
This Version
AM
Metadata
Show full item recordCitation
Vicary, J., Rice, A., Finster, E., & Reutter, D. (2022). A type theory for strictly unital infinity-categories. LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science https://doi.org/10.1145/3531130.3533363
Abstract
We use type-theoretic techniques to present an algebraic
theory of∞-categories with strict units. Starting with a known
type-theoretic presentation of fully weak ∞-categories, in
which terms denote valid operations, we extend the theory
with a non-trivial definitional equality. This forces some
operations to coincide strictly in any model, yielding the
strict unit behaviour.
We make a detailed investigation of the meta-theoretic
properties of this theory. We give a reduction relation that
generates definitional equality, and prove that it is confluent
and terminating, thus yielding the first decision procedure
for equality in a strictly-unital setting. Moreover, we show
that our definitional equality relation identifies all terms
in a disc context, providing a point comparison with a
previously proposed definition of strictly unital ∞-category.
We also prove a conservativity result, showing that every
operation of the strictly unital theory indeed arises from a
valid operation in the fully weak theory. From this, we infer
that strict unitality is a property of an ∞-category rather
than additional structure.
Sponsorship
EPSRC (EP/S018646/2)
Royal Society (RGF\R1\180097)
Royal Society (RGF\EA\180288)
Royal Society (UF160476)
Royal Society (RGF\EA\201079)
Identifiers
External DOI: https://doi.org/10.1145/3531130.3533363
This record's URL: https://www.repository.cam.ac.uk/handle/1810/336491
Statistics
Total file downloads (since January 2020). For more information on metrics see the
IRUS guide.