Andreas Nuyts, Higher pro-arrows: Towards a model for naturality pretype theory

Описание: Homotopy Type Theory Electronic Seminar Talks, 2024-05-02
https://www.uwo.ca/math/faculty/kapul...

In systems with internal parametricity, we get propagation and preservation of relations through/by all functions for free. In HoTT, we get preservation of equivalences by all functions for free. In directed type theory, we get preservation of morphisms by all (covariant) functions for free.
None of these three properties by itself is satisfactory: if we weaken equivalences or morphisms to relations, we lose their computational behaviour. If we want to rely on preservation of non-invertible morphisms, we need our functions to be covariant. And finally, simply not every morphism/relation is an equivalence.
We set out to develop a type system that has all three preservation properties in an interactive manner, so that we can preserve isomorphisms when available, morphisms when covariant, and relations as a last resort. Such a system should provide us with functoriality (fmap), parametricity and naturality proofs for free. I call such a system "Naturality Type Theory".
In this first step, I consider Naturality *Pre*type Theory: I defer all considerations of fibrancy to intuition and future work. In particular, I do not yet worry too much about the specifics of composition of and transport along morphisms.
By instantiating parametrized systems such as Multimod(e/al) Type Theory (MTT) and the Modal Transpension System (MTraS), we can moreover separate concerns and only worry about the presheaf model at every mode, and the modalities that we can model as adjunctions between these presheaf models, leaving syntactic matters to research on MTT and MTraS.
The presheaf models are designed to accommodate yet-to-be-defined higher pro-arrow equipments, and can be invented in three ways: (1) as a higher-dimensional version of pro-arrow equipments, (2) as a heterogenization of Tamsamani & Simpson's model of higher category theory, and (3) as a directification of Degrees of Relatedness.
In this talk, after motivating the subject, I intend to introduce the main ideas and then spiral towards the technical details, starting from the three existing settings/structures/models mentioned above.