arXiv · 0812.0298
Types are weak omega-groupoids
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.
Explore related subjects
Keep this discovery
Benno van den Berg, Richard Garner. 2008-12-01. Types are weak omega-groupoids. https://doi.org/10.1112/plms/pdq026
Cite the original work for its findings. Save a collection to share your selection of sources.