fact: Definition split_idempotent (c : C) : UU := ∑ (e : c --> c), is_split_idempotent e.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors