Added axiom export files.

Added files exporting witnesses for the axioms [Funext] and [Univalence], as per recent mailing list discussion.  Also (not in this commit request, but) provided documentation go with them on the HoTT/HoTT wiki: https://github.com/HoTT/HoTT/wiki/Using-the-HoTT-library .

Question: as we go on, providing/maintaining documentation for the library is fairly important.  Is it better to provide this on the HoTT/HoTT wiki (as above), or on the univalent-foundations wiki, or as extra files within the repo?