HoTT/HoTT — pull request #95 by peterlefanulumsdaine (2013-03-19 20:59:11+00:00)
Title: 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?