Abstract
We show that for any type in Martin-Löf Intensional Type Theory, the terms of that type and its higher identity types form a weak omega-category in the sense of Leinster. Precisely, we construct a contractible globular operad of definable composition laws, and give an action of this operad on the terms of any type and its identity types.
References
The reference list for this paper has not been collected yet.
Cited by
No paper in the index cites this yet (Semantic Scholar counts 117 in total).
The cited-by list is still filling in while reference lists are collected.