The ability to cast values between related types is a leitmotiv of many flavors of dependent type theory, such as observational type theories, subtyping, or cast calculi for gradual typing. These casts all exhibit a common structural behavior that boils down to the pervasive functoriality of type formers. We propose and extensively study a type theory, called AdapTT, which makes systematic and precise this idea of functorial type formers, with respect to an abstract notion of adapters relating types. Leveraging descriptions for functorial inductive types in AdapTT, we derive structural laws for type casts on general inductive type formers.

We define a naturality construction for the operations of weak ω-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 ω-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.

Abstract Weak $\omega$ -categories are notoriously difficult to define because of the very intricate nature of their axioms. Various approaches have been explored based on different shapes given to the cells. Interestingly, homotopy type theory encompasses a definition of weak $\omega$ -groupoid in a globular setting, since every type carries such a structure. Starting from this remark, Brunerie could extract this definition of globular weak $\omega$ -groupoids, formulated as a type theory. By refining its rules, Finster and Mimram have then defined a type theory called $\mathsf{CaTT}$ , whose models are weak $\omega$ -categories. Here, we generalize this approach to monoidal weak $\omega$ -categories. Based on the principle that they should be equivalent to weak $\omega$ -categories with only one 0-cell, we are able to derive a type theory $\mathsf{MCaTT}$ whose models are monoidal weak $\omega$ -categories. This requires changing the rules of the theory in order to encode the information carried by the unique 0-cell. The correctness of the resulting type theory is shown by defining a pair of translations between our type theory $\mathsf{MCaTT}$ and the type theory $\mathsf{CaTT}$ . Our main contribution is to show that these translations relate the models of our type theory to the models of the type theory $\mathsf{CaTT}$ consisting of $\omega$ -categories with only one 0-cell by analyzing in details how the notion of models interact with the structural rules of both type theories.