Aarhus University Seal

Directed type theory and homotopy theory

Paige North (Ohio State University)
Thursday 10 October 2019 16:15–17:00 Aud. D3 (1531-215)
Visiting Lecture
In this talk, I will describe the development of a directed type theory which can be used to describe directed homotopy theory and category theory. At the core of this type theory is a `homomorphism’ type former whose terms are meant to represent homomorphisms or directed paths. Its rules are roughly analogous to those of Martin-Löf’s identity type. I will give an interpretation of this type former in the category of small categories which helps to elucidate its rules. I will also describe directed variants of weak factorization systems for interpreting this type theory in categories of directed spaces.
Contact: Jacob Schach Møller Revised: 30.08.2019