May 2, Andreas Nuyts, Higher Pro-arrows: Towards a Model for Naturality Pretype Theory
Angiuli, Carlo
EDT (UTC-4) = 15:30 UTC.
This week we'll hear from Andreas Nuyts about "Higher Pro-arrows: Towards a
Model for Naturality Pretype Theory". The talk will be 60 minutes long, followed
by up to 30 minutes of discussion. The abstract is below.
The Zoom link is https://zoom.us/j/994874377
Videos and slides from past talks are available at:
https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html
Carlo
(On behalf of the HoTTEST organizers: Carlo Angiuli, Dan Christensen, Chris
Kapulkin, and Emily Riehl.)
--
Andreas Nuyts
Higher Pro-arrows: Towards a Model for Naturality Pretype Theory
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.