Agda development for "Parametricity, automorphisms of the universe, and excluded middle"

Paper: https://arxiv.org/abs/1701.05617 (actually this is a formalization of an unpublished newer version)

This code uses Agda's instance arguments to clarify which theorems rely on certain type-theoretical axioms such as function extensionality or univalence. To support these, use the ua-instance branch of abooij/HoTT-Agda.