We define a notion of weak ω-category internal to a model of Martin-Löf 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 ω-categories arising in this way are in fact ω-groupoids.
A preprint version of this paper may be downloaded here.