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