Parametricity, automorphisms of the universe, and excluded middle

Posted on 2017-01-26

In a cooperation between Martín Escardó, Peter Lumsdaine, Mike Shulman, and myself, we have strengthened the results from last year and recorded them in a paper that is now on arXiv.