Definition all_conjoints_setcat_profunctor_double_cat : all_conjoints_double_cat setcat_profunctor_double_cat. Proof. intros C₁ C₂ F. refine (representable_profunctor_right F ,, _). use make_double_cat_are_conjoints'. - exact (representable_profunctor_right_unit F). - exact (representable_profunctor_right_counit F). - abstract (use eq_profunctor_square ; intros y x h ; refine (transportf_disp_mor2_profunctors _ _ _ _ @ _) ; cbn ; etrans ; [ apply maponpaths ; apply (comp_v_profunctor_square_mor_comm (representable_profunctor_right_counit F) (representable_profunctor_right_unit F)) | ] ; rewrite lunitor_profunctor_nat_trans_mor_comm ; cbn ; rewrite !functor_id ; rewrite !id_left ; apply idpath). - abstract (use eq_profunctor_square ; intros y x h ; etrans ; [ apply transportf_disp_mor2_profunctors | ] ; cbn ; apply idpath). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Categories.CategoryOfSetCategories. Require Import UniMath.CategoryTheory.Categories.HSET.All. Require Import UniMath.CategoryTheory.Categories.HSET.SetCoends. Require Import UniMath.CategoryTheory.Profunctors.Core. Require Import UniMath.CategoryTheory.Profunctors.Examples. Require Import UniMath.CategoryTheory.Profunctors.Squares. Require Import UniMath.CategoryTheory.Profunctors.Transformation. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Isos. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Univalence. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Strictness. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.Examples.ProfunctorTwosidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.UnivalentDoubleCats. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints.