Directed homotopy type theory

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, and thus use it to study phenomena such as concurrency and rewriting. I will explain homotopy type theory in a way that motivates this generalization, so prior knowledge of homotopy type theory is not required.