proposition: Proposition to_equiv_implies_iso_equiv {C : Category} {x y} (f g : x ≅ y) : to f ≈ to g -> f ≈ g.
proof: Proof. intro eq. split; [ assumption | ]. assert (m := iso_to_epic f). destruct f as [tof fromf tofrom_eqf fromto_eqf], g as [tog fromg tofrom_eqg fromto_eqg]. simpl in *. destruct m as [epic]. apply epic. rewrite fromto_eqf, eq, fromto_eqg; reflexivity. Qed.
imports: Category.Lib Category.Theory.Category Category.Theory.Morphisms