HoTT/HoTT — pull request #113 by peterlefanulumsdaine (2013-03-29 18:42:53+00:00)
Title: Added exploit for polymorphic axioms

As per recent discussions, working with monomorphic axioms is quite cumbersome; so am adding (until true polymorphic axioms are available) the exploit that seems (so far, at least) to fake them. So: if you want polymorphic axioms in your development, use `Require Import FunextAxiom`, and so on.

The preferred library style is still to restrict axioms within sections (since a global assumption irrevocably pollutes any development importing the library). However, Bas argues strongly that in some of his contributions (e.g. on the object classifier), it’s very cumbersome to do this, because of the monomorphism problem; so he would like to import `FunextAxiom` within a few specific library files. My feeling is that this is OK, provided it’s clearly documented in those files (and I guess that we keep them out of the `HoTT.v` export list for now). Another option would be to say: for now, files doing this should stay in `/contrib`. Thoughts?