Axiom removal

Remove all internal uses of `FunextAxiom` and `UnivalenceAxiom`.  For me, with the latest version of HoTT/coq, everything works fine without them.

Once again, I can get rid of the whitespace changes that my emacs made.