fact: Definition retract {x y x' y' : C} (f : x --> y) (f' : x' --> y') : UU := ∑ (ix : x' --> x) (rx : x --> x') (iy : y' --> y) (ry : y --> y'), is_retract f f' ix rx iy ry.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat