Category Archives: Uncategorized
I have often seen competent mathematicians and logicians, outside our circle, making technically erroneous comments about the univalence axiom, in conversations, in talks, and even in public material, in journals or the web. For some time I was a bit … Continue reading
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