Definition all_companions_univcat_profunctor_verity_double_bicat : all_companions univcat_profunctor_verity_double_bicat. Proof. refine (λ (C₁ C₂ : univalent_category) (F : C₁ ⟶ C₂), representable_profunctor_left F ,, _). use make_are_companions ; cbn. - apply representable_profunctor_left_unit. - apply representable_profunctor_left_counit. - abstract (use eq_profunctor_square ; intros y x h ; cbn in * ; etrans ; [ apply maponpaths ; apply (comp_v_profunctor_square_mor_comm (representable_profunctor_left_counit F) (representable_profunctor_left_unit F)) | ] ; rewrite runitor_profunctor_nat_trans_mor_comm ; cbn ; rewrite !functor_id ; rewrite !id_right ; apply idpath). - abstract (use eq_profunctor_square ; intros y x h ; cbn in * ; rewrite !id_left, !id_right ; 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.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.UnivalenceOp. Require Import UniMath.Bicategories.Core.Examples.OpCellBicat. Require Import UniMath.Bicategories.Core.Examples.BicatOfUnivCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.