proposition: Lemma functor_on_retract {C D : category} (F : functor C D) {x y x' y' : C} {f : x --> y} {f' : x' --> y'} (r : retract f f') : retract (#F f) (#F f').
proof: Proof. destruct r as [ix [ra [iy [ry [hx [hy [hi hr]]]]]]]. use (make_retract (#F ix) (#F ra) (#F iy) (#F ry)). use make_is_retract; repeat rewrite <- functor_comp; try rewrite <- functor_id. - now rewrite hx. - now rewrite hy. - now rewrite hi. - now rewrite hr. Defined.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat