Definition id_are_companions {B : verity_double_bicat} (x : B) : are_companions (id_h x) (id_v x). Proof. use make_are_companions. - apply id_v_square_bicat. - apply id_v_square_bicat. - abstract (refine (_ @ rwhisker_square_id _ _) ; rewrite <- rinvunitor_runitor ; rewrite rwhisker_square_comp ; apply maponpaths ; rewrite id_h_square_bicat_id ; rewrite lunitor_v_comp_square' ; rewrite rwhisker_lwhisker_square ; rewrite <- lwhisker_square_comp ; rewrite linvunitor_lunitor ; rewrite lwhisker_square_id ; rewrite lunitor_V_id_is_left_unit_V_id ; apply idpath). - abstract (refine (_ @ dwhisker_square_id _ _) ; rewrite <- rinvunitor_runitor ; rewrite dwhisker_square_comp ; apply maponpaths ; rewrite <- !id_h_square_bicat_id ; rewrite lunitor_h_comp_square' ; rewrite dwhisker_uwhisker_square ; rewrite <- uwhisker_square_comp ; rewrite linvunitor_lunitor ; rewrite uwhisker_square_id ; rewrite lunitor_V_id_is_left_unit_V_id ; 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.Unitors. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Univalence. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Morphisms.Adjunctions. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.VerityDoubleBicat. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.DerivedLaws. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.CellsAndSquares. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.UnderlyingCats. Require Import UniMath.Bicategories.DoubleCategories.DoubleBicat.LocalUnivalence. Require Import UniMath.Bicategories.DoubleCategories.Examples.TransposeDoubleBicat.