University of Birmingham > Talks@bham > Theoretical computer science seminar > A homotopy type theory for directed homotopy theory

A homotopy type theory for directed homotopy theory

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Dan Ghica.

In this talk, I will propose a directed type theory. The goal of this project is to develop a 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 progress towards constructing weak factorization systems and interpretations in categories of directed spaces.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on talks.cam from the University of Cambridge.