Category Archives: Uncategorized
I recently completed my master’s thesis under the supervision of Steve Awodey and Jonas Frey. A copy can be found here. Known impredicative encodings of various inductive types in System F, such as the type of natural numbers do not … Continue reading
Some months ago I gave a series of hands-on lectures on cubicaltt at Inria Sophia Antipolis that can be found at: https://github.com/mortberg/cubicaltt/tree/master/lectures The lectures cover the main features of the system and don’t assume any prior knowledge of Homotopy Type … Continue reading
This post is to announce a new article that I recently uploaded to the arxiv: https://arxiv.org/abs/1701.07538 The main result of that article is a type theoretic replacement construction in a univalent universe that is closed under pushouts. Recall that in … Continue reading
From June 4 — 10, 2017, there will be a workshop on homotopy type theory as one of the AMS’s Mathematical Research Communities (MRCs).
Almost at the top of the HoTT website are the words: “Homotopy Type Theory refers to a new interpretation of Martin-Löf’s system of intensional, constructive type theory into abstract homotopy theory. ” I think it is time to change these words … Continue reading