Tashi Walde: Synthetic category theory II: Martin-Löf approach

Speaker
Tashi Walde, University of Regensburg

Abstract
To showcase one possible path towards instantiating synthetic category theory as explained in Bastiaan’s talk, I will sketch a type theory partially developed by my master student Riva extending HoTT. Compared to other related type theories for synthetic category theory, the main advantage is that all types are categories; the main price to pay is that one has to restrict the formation of dependent products.