A type theory for strictly unital infinity ∞-categories

Eric Finster; David Reutter; Alex Rice; Jamie Vicary

doi:10.48550/arXiv.2007.08307

A type theory for strictly unital infinity ∞-categories

Eric Finster, David Reutter, Alex Rice, Jamie Vicary

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

Abstract / Description of output

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.

Original language	English
Title of host publication	LICS '22
Subtitle of host publication	Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
Editors	Christel Baier
Place of Publication	New York, NY, USA
Publisher	ACM
Pages	1-12
Number of pages	12
ISBN (Electronic)	9781450393515
DOIs	https://doi.org/10.48550/arXiv.2007.08307 https://doi.org/10.1145/3531130.3533363
Publication status	Published - 4 Aug 2022
Event	The Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science - Technion, Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022 Conference number: 37 https://lics.siglog.org/lics22/

Publication series

Name	Proceedings of the ACM/IEEE Annual Symposium on Logic in Computer Science
Publisher	ACM
ISSN (Print)	1043-6871
ISSN (Electronic)	2575-5528

Symposium

Symposium	The Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science
Abbreviated title	LICS 2022
Country/Territory	Israel
City	Haifa
Period	2/08/22 → 5/08/22
Internet address	https://lics.siglog.org/lics22/

Keywords / Materials (for Non-textual outputs)

higher category theory
semistrictness

Access to Document

FinsterEtalLICS2022ATypeTheoryForStrictlyUnitalAccepted author manuscript, 487 KB

Cite this

Finster, E., Reutter, D., Rice, A., & Vicary, J. (2022). A type theory for strictly unital infinity ∞-categories. In C. Baier (Ed.), LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (pp. 1-12). Article 48 (Proceedings of the ACM/IEEE Annual Symposium on Logic in Computer Science). ACM. https://doi.org/10.48550/arXiv.2007.08307, https://doi.org/10.1145/3531130.3533363

@inproceedings{ec278119e7ca44ba969b8d4d09c4f04c,

title = "A type theory for strictly unital infinity ∞-categories",

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

keywords = "higher category theory, semistrictness",

author = "Eric Finster and David Reutter and Alex Rice and Jamie Vicary",

year = "2022",

month = aug,

day = "4",

doi = "10.48550/arXiv.2007.08307",

language = "English",

series = "Proceedings of the ACM/IEEE Annual Symposium on Logic in Computer Science",

publisher = "ACM",

pages = "1--12",

editor = "Christel Baier",

booktitle = "LICS '22",

note = "The Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 ; Conference date: 02-08-2022 Through 05-08-2022",

url = "https://lics.siglog.org/lics22/",

}

Finster, E, Reutter, D, Rice, A & Vicary, J 2022, A type theory for strictly unital infinity ∞-categories. in C Baier (ed.), LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science., 48, Proceedings of the ACM/IEEE Annual Symposium on Logic in Computer Science, ACM, New York, NY, USA, pp. 1-12, The Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, 2/08/22. https://doi.org/10.48550/arXiv.2007.08307, https://doi.org/10.1145/3531130.3533363

A type theory for strictly unital infinity ∞-categories. / Finster, Eric; Reutter, David; Rice, Alex et al.
LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. ed. / Christel Baier. New York, NY, USA: ACM, 2022. p. 1-12 48 (Proceedings of the ACM/IEEE Annual Symposium on Logic in Computer Science).

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

TY - GEN

T1 - A type theory for strictly unital infinity ∞-categories

AU - Finster, Eric

AU - Reutter, David

AU - Rice, Alex

AU - Vicary, Jamie

N1 - Conference code: 37

PY - 2022/8/4

Y1 - 2022/8/4

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

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

KW - higher category theory

KW - semistrictness

U2 - 10.48550/arXiv.2007.08307

DO - 10.48550/arXiv.2007.08307

M3 - Conference contribution

T3 - Proceedings of the ACM/IEEE Annual Symposium on Logic in Computer Science

SP - 1

EP - 12

BT - LICS '22

A2 - Baier, Christel

PB - ACM

CY - New York, NY, USA

T2 - The Thirty-Seventh Annual ACM/IEEE Symposium on Logic in Computer Science

Y2 - 2 August 2022 through 5 August 2022

ER -

Finster E, Reutter D, Rice A, Vicary J. A type theory for strictly unital infinity ∞-categories. In Baier C, editor, LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science. New York, NY, USA: ACM. 2022. p. 1-12. 48. (Proceedings of the ACM/IEEE Annual Symposium on Logic in Computer Science). doi: 10.48550/arXiv.2007.08307, 10.1145/3531130.3533363

A type theory for strictly unital infinity ∞-categories

Abstract / Description of output

Publication series

Symposium

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Cite this