HoTT/HoTT — pull request #135 by JasonGross (2013-07-05 03:15:27+00:00)
Title: Stick [Context `{Funext}.] inside a section

[Context] is only meant to be used for local assumptions, not axioms.
And this file doesn't import the funext axiom file, so I assume this is
meant to be local.

Once again, emacs has removed trailing space; I can strip those changes from this commit if desired.