A type theory for strictly unital infinity-categories
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
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.
Description
Keywords
Journal Title
Conference Name
Journal ISSN
Volume Title
Publisher
Publisher DOI
Rights
Sponsorship
Royal Society (RGF\R1\180097)
Royal Society (RGF\EA\180288)
Royal Society (UF160476)
Royal Society (RGF\EA\201079)