Definition comp_are_companions {B : verity_double_bicat} {x y z : B} {h₁ : x --> y} {h₂ : y --> z} {v₁ : x -|-> y} {v₂ : y -|-> z} (c₁ : are_companions h₁ v₁) (c₂ : are_companions h₂ v₂) : are_companions (h₁ · h₂) (v₁ · v₂). Proof. use make_are_companions. - exact (comp_are_companions_unit c₁ c₂). - exact (comp_are_companions_counit c₁ c₂). - exact (comp_are_companions_left c₁ c₂). - abstract (refine (_ @ comp_are_companions_left (B := transpose_verity_double_bicat B) (companions_to_transpose c₁) (companions_to_transpose c₂)) ; do 2 apply maponpaths ; cbn ; unfold comp_are_companions_counit, comp_are_companions_unit ; cbn ; rewrite lwhisker_uwhisker_square ; rewrite !double_bicat_interchange ; apply maponpaths ; rewrite rwhisker_dwhisker_square ; 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.