Prove uniqueness of homotopy and equivalence induction

[fredrik-bakke]

From this, it follows that having pairs (eq-htpy , is-section-eq-htpy) and (eq-equiv , is-section-eq-equiv) are propositions, so we can remove the redundant postulates is-retraction-eq-(htpy|equiv)' and coh-eq-(htpy|equiv)' as introduced in #1119.