Definition make_data_of_profunctor : functor_data (category_binproduct C₂^op C₁) HSET. Proof. use make_functor_data. - refine (λ xy, make_hSet (pr1 F (pr1 xy) (pr2 xy)) _). apply HF. - exact (λ xy₁ xy₂ fg h, pr2 F _ _ (pr1 fg) _ _ (pr2 fg) h). Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.Categories.HSET.All.