Definition homSet_functor_data : functor_data (category_binproduct (C^op) C) hset_category. Proof. use make_functor_data. + intros pair. induction pair as (p1, p2). use make_hSet. - exact (C ⟦ p1, p2 ⟧). - use (homset_property C). + intros x y fg h. induction fg as (fg1, fg2). cbn in fg1. exact (fg1 · h · fg2). 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.