Lemma functor_preserves_is_split_idempotent {c : C} (f : split_idempotent c) : is_split_idempotent (#F f). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.OppositeCategory.Core.