LFCS Seminar: 1 June 2021 - Paige North

Title: Directed Homotopy Type Theory

Abstract:

In this talk, I will describe the development of a directed homotopy type theory. The aim is to capture (higher) categories and directed topological spaces as models of the theory. To get this, the identity type of Martin-Löf is modified to produce a 'directed’ identity type. The terms of this new directed identity type behave analogously to those of the usual Martin-Löf identity type: they can be composed, but not inverted. This has semantics in the category of categories in which the directed identity type is interpreted by hom-sets [1].

I will also talk about work-in-progress in which techniques of modal type theory are used to modify the underlying syntax to allow for different kinds of transport: forward along directed identities, backward along directed identities, and along (usual, undirected) identities. These are reflected in the semantics, for example in Cat, as the lifting properties of Grothendieck opfibrations, fibrations, and isofibrations. 

Affiliates: Paige North, University of Pennsylvania

https://paigenorth.github.io/

 [1]  https://doi.org/10.1016/j.entcs.2019.09.012