Definition all_companions_two_cat_square_double_cat (C : two_cat) : all_companions_double_cat (two_cat_square_double_cat C). Proof. intros x y f. refine (f ,, _). use make_double_cat_are_companions'. - apply id2. - apply id2. - abstract (cbn ; rewrite id2_rwhisker ; rewrite lwhisker_id2 ; rewrite !id2_right ; rewrite <- !lwhisker_vcomp ; rewrite <- !rwhisker_vcomp ; refine (transportf_disp_mor2_two_cat_arrow _ _ _ _ @ _) ; unfold two_cat_lassociator, two_cat_rassociator ; unfold two_cat_runitor, two_cat_rinvunitor ; unfold two_cat_lunitor, two_cat_linvunitor ; rewrite !vassocl ; rewrite !idto2mor_lwhisker ; rewrite !idto2mor_rwhisker ; rewrite !idto2mor_comp ; apply maponpaths ; apply (homset_property C)). - abstract (cbn ; rewrite id2_rwhisker ; rewrite lwhisker_id2 ; rewrite !id2_right ; refine (transportf_disp_mor2_two_cat_arrow _ _ _ _ @ _) ; unfold two_cat_lassociator, two_cat_rassociator ; unfold two_cat_runitor, two_cat_rinvunitor ; unfold two_cat_lunitor, two_cat_linvunitor ; rewrite !vassocl ; rewrite !idto2mor_lwhisker ; rewrite !idto2mor_rwhisker ; rewrite !idto2mor_comp ; apply maponpaths ; apply (homset_property C)). Defined.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Prelude. Require Import UniMath.CategoryTheory.Core.Setcategories. Require Import UniMath.CategoryTheory.Core.TwoCategories. Import TwoCategories.Notations. 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.SquaresTwoCat. Require Import UniMath.Bicategories.DoubleCategories.Basics.StrictDoubleCatBasics. 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.PseudoDoubleSetCats. Require Import UniMath.Bicategories.DoubleCategories.Core.CompanionsAndConjoints.