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: 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