fact: Definition FunctorPrecatMorToNatTrans {c c': functor_precategory (opp_precat C) HSET has_homsets_HSET} (h : c --> c') : nat_trans (FunctorPrecatObToFunctor c) (FunctorPrecatObToFunctor c') := h.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Equalizers UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.slicecat UniMath.CategoryTheory.Monics UniMath.CategoryTheory.Subobjects UniMath.CategoryTheory.yoneda UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Limits.Graphs.Pullbacks UniMath.CategoryTheory.Limits.Graphs.Equalizers UniMath.CategoryTheory.Subcategory.Core UniMath.CategoryTheory.Subcategory.Full UniMath.CategoryTheory.Equivalences.Core