Naturality for higher-dimensional path types
Naturality for higher-dimensional path types
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, and we realise it as a globular analogue of Reynolds parametricity. Our construction operates as a "power tool" to support …