A bunched approach to directed HoTT
, Chocola, ENS Lyon, France
A presentation of Bunched Affine Type Theory (BATT).
This work is part of my thesis, under the supervision of Samuel Mimram.
abstract:
The last two decades have seen the emergence of “homotopy” type theory (HoTT), in which intensional identity types can be interpreted as the space of paths connecting two points of a type. This new interpretation allows types in HoTT to be viewed as spaces up to homotopy, thereby providing a synthetic language well-suited to formalizing results specific to homotopy theory or to drawing parallels between mathematical logic and that field. More recently, we have seen the emergence of a variant of HoTT that allows us to work with a notion of “directed” spaces, up to homotopy — think of how directed graphs relate to undirected graphs. Within this setting, there is a concept of (directed) path types between two points of a given type, which in turn cannot yet be a directed space. We will explore an idea to remedy this shortcoming and enable the study of a higher version of directedness, where path types of directed types can themselves be directed (∞-groupoids). We will see along the way why it may be useful to consider an extension of the syntax where two kinds of context extensions coexist, akin to the Cartesian and linear pairing of contexts appearing in linear logic. The new pairing operation is being thought about as the Gray tensor product of categories, and its adjoints are to be interpreted as the categories of functors together with lax (resp. oplax) transformations. Such a system is known as “bunched logic” or “bunched type theory”. We will present a draft version of its rules and simple examples of its usefulness, for instance, in order to define the directed path type of a type.