Naturality for higher-dimensional path types

TL;DR

This paper introduces a naturality construction for weak omega-categories within dependent type theory, enabling the creation of complex geometrical terms and composition operations, with implementation verified in a proof assistant.

Contribution

It presents a novel naturality construction for weak omega-categories, inspired by geometrical intuition, and implements it in a proof assistant to support complex term generation.

Findings

Construction supports complex geometrical terms

Implementation verifies correctness of generated terms

Enables explicit computation of path type inhabitants

Abstract

We define a naturality construction for the operations of weak omega-categories, as a meta-operation in a dependent type theory. Our construction has a geometrical motivation as a local tensor product with a directed interval, and behaves logically as a globular analogue of Reynolds parametricity. Our construction operates as a ``power tool'' to support construction of terms with geometrical structure, and we use it to define composition operations for cylinders and cones in omega-categories. The machinery can generate terms of high complexity, and we have implemented our construction in a proof assistant, which verifies that the generated terms have the correct type. All our results can be exported to homotopy type theory, allowing the explicit computation of complex path type inhabitants.