Added exploit for polymorphic axioms.
Merge pull request #113 from peterlefanulumsdaine/master

Added exploit for polymorphic axioms
adapt to the new version of coqtop by disabling the native compiler
Merge pull request #114 from ybertot/master

Make the library work with the current version of HoTT/coq trunk
Adding Object Classifier, Unique choice and a general coherence lemma for UA.
epis are surjective