Changes the postulates for funext and univalence such that there is judgmentally only one converse map to htpy-eq and equiv-eq. The main benefit, however, is that now eq-htpy and eq-equiv will appear with their own names in Agda interactive mode, rather than as pr1 (pr1 (funext ... ...)) and pr1 (pr1 (univalence ... ...)).
I leave it for potential future work to prove is-retraction-eq-(equiv|htpy)' and coh-eq-(equiv|htpy)' rather than postulate them, if we want this. Note that we could get away with even fewer postulates if we really wanted to (see TypeTopology/UF.Lower-FunExt).
Changes the postulates for funext and univalence such that there is judgmentally only one converse map to
htpy-eqandequiv-eq. The main benefit, however, is that noweq-htpyandeq-equivwill appear with their own names in Agda interactive mode, rather than aspr1 (pr1 (funext ... ...))andpr1 (pr1 (univalence ... ...)).I leave it for potential future work to prove
is-retraction-eq-(equiv|htpy)'andcoh-eq-(equiv|htpy)'rather than postulate them, if we want this. Note that we could get away with even fewer postulates if we really wanted to (seeTypeTopology/UF.Lower-FunExt).