Definition hom_functor_data : functor_data (precategory_binproduct (opp_precat C) C) type_precat. Proof. use make_functor_data. - intros pair; exact (C ⟦ pr1 pair, pr2 pair ⟧). - intros x y fg h. refine (_ · h · _). + exact (pr1 fg). + exact (pr2 fg). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.UnivalenceAxiom. 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.