Use polymorphic [Axiom]s, not the [admit] exploit

The newer versions of HoTT/coq support polymorphic axioms, and no longer
require the [admit] exploit.  This way, we have two fewer top-level
constants floating around.