(1) Restructure all the directories and files.
(2) Space.Interval is added.
(3) Tagged as v0.1.0.
A short proof of abelianness of Omega2(A).
Pi1(S1) = Z and other cleanups
The proof for Pi1(S1) = Z was completed, along with
lots of other cleanups. I might merge Interger.agda
back into Prelude.agda later.
Dramatic changes from the previous version
(1) Departing from Nils' library and giving up
propositional computational rules for J.
(2) The proof for the total space of Hopf-junior
(3) There are still some holes to be filled in. See
Preimage.agda and Univalence/Extensionality.agda