Types are weak ω-groupoids
Publication date
2011-02
Authors
van den Berg, B.
Garner, R.
Editors
Advisors
Supervisors
Document Type
Article
Metadata
Show full item recordCollections
License
Abstract
We define a notion of weak omega-category internal to a model of Martin-L\"of type theory, and prove that each type bears a canonical weak omega-category structure obtained from the tower of iterated identity types over that type. We show that the omega-categories arising in this way are in fact omega-groupoids
Keywords
Wiskunde en Informatica (WIIN), Mathematics, Landbouwwetenschappen, Natuurwetenschappen, Wiskunde: algemeen
Citation
van den Berg, B & Garner, R 2011, 'Types are weak ω-groupoids', Proceedings of the London Mathematical Society, vol. 102, no. 2, pp. 370-394. https://doi.org/10.1112/plms/pdq026