English
 
Help Privacy Policy Disclaimer
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

A type theory for strictly unital ∞-categories

MPS-Authors
/persons/resource/persons284603

Reutter,  David       
Max Planck Institute for Mathematics, Max Planck Society;

Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)
There are no public fulltexts stored in PuRe
Supplementary Material (public)
There is no public supplementary material available
Citation

Finster, E., Reutter, D., Rice, A., & Vicary, J. (2022). A type theory for strictly unital ∞-categories. In C. Baier (Ed.), Proceedings of the Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2022). New York, NY: Association for Computing Machinery.


Cite as: https://hdl.handle.net/21.11116/0000-0010-5051-8
Abstract
We use type-theoretic techniques to present an algebraic theory of
$\infty$-categories with strict units. Starting with a known type-theoretic
presentation of fully weak $\infty$-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 $\infty$-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 $\infty$-category rather than additional structure.