Open fredrik-bakke opened 2 months ago
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.
(eq-htpy , is-section-eq-htpy)
(eq-equiv , is-section-eq-equiv)
is-retraction-eq-(htpy|equiv)'
coh-eq-(htpy|equiv)'
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 postulatesis-retraction-eq-(htpy|equiv)'andcoh-eq-(htpy|equiv)'as introduced in #1119.