proposition: Lemma retract_is_iso {x y x' y' : C} {f : iso x y} {f' : x' --> y'} (r : retract f f') : is_iso f'.
proof: Proof. destruct r as [ix [rx [iy [ry [hx [hy [hi hr]]]]]]]. apply is_iso_from_is_z_iso. exists (iy · (inv_from_iso f) · rx). split. - rewrite assoc, assoc, <- hi. rewrite <- (assoc ix _ _). rewrite iso_inv_after_iso, id_right. exact hx. - rewrite <- assoc, <- assoc, hr, assoc, assoc. rewrite <- (assoc iy _ _). rewrite iso_after_iso_inv, id_right. exact hy. Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat