1) If two maps A' -> A and B' -> B are equivalent, in the sense that we have a homotopy commutative square both of whose maps are equivalences, then if one is an equivalence then so is the other.
2) For this I needed cancellation statements for is-equiv, previously called is-equiv-left-factor and is-equiv-right-factor, which so far were only implemented in the later file 08-families-of-maps.rzk.md using constructions therein.
I wrote a new implementation called is-equiv-left-cancel and is-equiv-right-cancel (the latter already in an earlier PR, since at the time I hadn't realised that is-equiv-right-factor already existed). This implementation is more elementary and arguably simpler, so that I could place it in the file 03-equivalences.rzk.md, where I believe it belongs. Moreover, it is slightly stronger, since it does not require that the map that gets cancelled is an equivalence, but only a retraction/section. I have now simply redefined the *-factor ones in terms of the *-cancel ones. They are probably worth keeping since one often only cares about equivalences so that having to extract the section/retraction would just be a hassle.
1) If two maps
A' -> AandB' -> Bare equivalent, in the sense that we have a homotopy commutative square both of whose maps are equivalences, then if one is an equivalence then so is the other.2) For this I needed cancellation statements for
is-equiv, previously calledis-equiv-left-factorandis-equiv-right-factor, which so far were only implemented in the later file08-families-of-maps.rzk.mdusing constructions therein. I wrote a new implementation calledis-equiv-left-cancelandis-equiv-right-cancel(the latter already in an earlier PR, since at the time I hadn't realised thatis-equiv-right-factoralready existed). This implementation is more elementary and arguably simpler, so that I could place it in the file03-equivalences.rzk.md, where I believe it belongs. Moreover, it is slightly stronger, since it does not require that the map that gets cancelled is an equivalence, but only a retraction/section. I have now simply redefined the*-factorones in terms of the*-cancelones. They are probably worth keeping since one often only cares about equivalences so that having to extract the section/retraction would just be a hassle.