proposition: Lemma is_functor_Under_mor_functor_data {c c' : C} (h : C⟦c, c'⟧) : is_functor (Under_precategories_mor_functor_data h).
proof: Proof. split. - intro. apply (Under_mor_equality _ hs). apply idpath. - intros ? ? ? ? ?. apply (Under_mor_equality _ hs). apply idpath. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors