Definition all_companions_square_verity_double_bicat : all_companions square_verity_double_bicat. Proof. intros x y f. refine (f ,, _). use make_are_companions ; cbn. - apply id2. - apply id2. - abstract (rewrite id2_rwhisker, lwhisker_id2, !id2_right ; rewrite lassociator_rassociator ; rewrite id2_left ; rewrite lunitor_triangle ; rewrite vcomp_lunitor ; apply idpath). - abstract (rewrite id2_rwhisker, lwhisker_id2, !id2_right ; rewrite rassociator_lassociator ; rewrite id2_left ; rewrite !vassocl ; rewrite runitor_triangle ; rewrite vcomp_runitor ; apply idpath). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.TwoSidedDisplayedCats.TwoSidedDispCat. Require Import UniMath.Bicategories.Core.Bicat. Import Bicat.Notations. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.EquivToAdjequiv. Require Import UniMath.Bicategories.Core.AdjointUnique. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.Core.