Monthly Archives: January 2017
Type theoretic replacement & the n-truncation
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
Posted in Uncategorized
Leave a comment
Parametricity, automorphisms of the universe, and excluded middle
Specific violations of parametricity, or existence of non-identity automorphisms of the universe, can be used to prove classical axioms. The former was previously featured on this blog, and the latter is part of a discussion on the HoTT mailing list. In a cooperation … Continue reading
Posted in Foundations
7 Comments
Homotopy Type Theory 