editing notes added for funny symbols
a more suggestive notation for nested coproducts
renamed hott.core.pair to hott.core.sigma
expose Eckmann-Hilton to the outside world.