proposition: Lemma has_homsets_wosetfun_precategory : has_homsets wosetfun_precategory.
proof: Proof. intros X Y. apply (isasetsubset (pr1wofun X Y)). - apply isaset_set_fun_space. - apply isinclpr1; intro f. apply isaprop_iswofun. Qed.
imports: UniMath.MoreFoundations.All UniMath.Combinatorics.OrderedSets UniMath.Combinatorics.WellOrderedSets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Setcategories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.exponentials