TY - RPRT TI - Parametricity, automorphisms of the universe, and excluded middle AU - Auke Bart Booij AU - Martín Hötzel Escardó AU - Peter LeFanu Lumsdaine AU - Michael Shulman PY - 2017 UR - https://arxiv.org/abs/1701.05617 ID - 1701.05617 ER -