Lemma is_functor_homSet_functor_type : is_functor homSet_functor_data. Proof. use make_dirprod. - intro; cbn. apply funextsec; intro. refine (id_right _ @ _). apply id_left. - repeat intro. apply funextsec; intro; cbn. do 3 rewrite assoc. reflexivity. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.UnivalenceAxiom. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Foundations.HLevels. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.