fact: Definition functor_preserves_idempotent {c : C} (H : idempotent c) : idempotent (F c) := _ ,, functor_preserves_is_idempotent H.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors