Types are weak omega-groupoids
Logic
2011-10-17 v2 Category Theory
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
Cite
@article{arxiv.0812.0298,
title = {Types are weak omega-groupoids},
author = {Benno van den Berg and Richard Garner},
journal= {arXiv preprint arXiv:0812.0298},
year = {2011}
}
Comments
28 pages; v2: final journal version