Types are weak omega-groupoids

TL;DR

This paper introduces a framework for weak omega-categories within Martin-Löf type theory, demonstrating that types naturally possess omega-groupoid structures derived from iterated identity types.

Contribution

It defines weak omega-categories internally in type theory and proves these structures are omega-groupoids, linking type-theoretic constructs with higher category theory.

Findings

Types have a canonical weak omega-category structure

The constructed omega-categories are in fact omega-groupoids

The structure is obtained from iterated identity types

Abstract

We define a notion of weak omega-category internal to a model of Martin-L\"of 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 omega-categories arising in this way are in fact omega-groupoids.