I have adapted some basic HoTT theorems and proofs to prose form, in an attempt to better understand the results and their proofs. The Coq proof scripts often obscure details of the exposition, like the choice of fibration in an induction tactic, or run the argument backwards in a mathematically awkward way. At times they also duplicate proofs that are completely symmetric, or choose an easily mechanizable but somewhat unnatural argument.
Of course these are all matters of taste, but I at least thought it would be worth a try to “mathematize” the arguments and notation. (I have nothing against Coq proofs except that they’re not well-suited for human consumption!) I think the result is pretty readable, and Dan Licata has pointed out that this could be a useful resource for anyone interested in porting these proofs to a different system.
The file covers results from path concatenation through function extensionality. I closely follow Andrej Bauer’s Coq proof scripts, which are in turn based on Voevodsky’s. I have taken minor liberties and invented some notation. (Does anyone have better notation for transport?) I’m hoping to continue adding results to this file, starting with Mike Shulman’s proof of .
Here’s the PDF. (Added section 4, 3/26/12.)