proposition: Lemma functor_preserves_is_split_idempotent {c : C} (f : split_idempotent c) : is_split_idempotent (#F f).
proof: Proof. unfold is_split_idempotent. exists (F (split_idempotent_object f)). exists (functor_preserves_retraction (split_idempotent_retraction f)). refine (_ @ functor_comp _ _ _). apply maponpaths. apply split_idempotent_is_split. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors