Weak omega-categories from intensional type theory

TL;DR

This paper demonstrates that types in Martin-Löf Intensional Type Theory inherently form weak omega-categories by constructing a contractible globular operad and showing its action on these types and their identity types.

Contribution

It introduces a novel construction of a contractible globular operad that models the weak omega-category structure within intensional type theory.

Findings

Types and their higher identity types form weak omega-categories

Constructed a contractible globular operad of composition laws

Established an action of the operad on types and identity types

Abstract

We show that for any type in Martin-L\"of 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.