You can clone with
HTTPS or Subversion.
Show free groups are groups.
- Use 'append' directly instad of 'rev-append'.
- Finish the interface of a group.
Name changes. (Following Chris' suggestions.)
Bijection -> H-equivalence
Preimage -> H-fiber
(1) Restructure all the directories and files.
(2) Space.Interval is added.
(3) Tagged as v0.1.0.
Minor changes in comments
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