Abstract
We define a notion of weak ω-category internal to a model of Martin-Löf's type theory, and prove that each type bears a canonical weak ω-category structure obtained from the tower of iterated identity types over that type. We show that the ω-categories arising in this way are in fact ω-groupoids.
Original language | English |
---|---|
Pages (from-to) | 370-394 |
Number of pages | 25 |
Journal | Proceedings of the London Mathematical Society |
Volume | 102 |
Issue number | 2 |
DOIs | |
Publication status | Published - Feb 2011 |
Externally published | Yes |