removed spurious dependency
added type former equivalences for the empty type
generalized some definitions in order to add a missing equivalence
added missing \eta-law and equivalence for \down-Pi-out
added equivalences for commutativity of products
added more equivalences for function composition
added more equivalences for path composition
refactoring path composition equivalences
Merge branch 'master' of git://github.com/sattlerc/HoTT-Agda into sattlerc-master

Conflicts:
	lib/Equivalences.agda
Merge branch 'sattlerc-master'
lib.types.Nat: export injectivity of S, close #12
Merge pull request #14 from mikeshulman/S-injective

lib.types.Nat: export injectivity of S, close #12