Aarhus University Seal / Aarhus Universitets segl

Directed type theory and homotopy theory

Paige North (Ohio State University)
Visiting Lecture
Thursday, 10 October, 2019, at 16:15-17:00, in Aud. D3 (1531-215)
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 person: Jacob Schach Møller