Higher-dimensional categories have recently emerged as a natural context for modelling intensional type theories; this raises the question of what higher-categorical structures the syntax of type theory naturally forms. We show that for any type in Martin-Loef Intensional Type Theory, the system of terms of that type and its higher identity types forms a weak ω-category in the sense of Leinster. Precisely, we construct a contractible globular operad P_(ML~(Id)) of type-theoretically definable composition laws, and give an action of this operad on any type and its identity types.
展开▼
