Definition make_double_cat_are_companions' {C : double_cat} {x y : C} {h : x -->h y} {v : x -->v y} (φ : square v (identity_v y) h (identity_h y)) (ψ : square (identity_v x) v (identity_h x) h) (p : transportf_square (id_v_right _ @ id_v_right _) (id_v_right _ @ id_v_right _) ((linvunitor_h h ⋆v (ψ ⋆h φ)) ⋆v runitor_h h) = id_v_square h) (q : transportf_square (id_left _) (id_right _) (ψ ⋆v φ) = id_h_square v) : double_cat_are_companions h v. Proof. refine (φ ,, ψ ,, _ ,, _). - abstract (rewrite transportf_square_prewhisker ; rewrite transportf_f_square ; refine (_ @ p) ; use transportf_square_eq ; apply idpath). - abstract (refine (_ @ q) ; rewrite transportf_f_square ; use transportf_square_eq ; 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.DoubleCategories.Basics.DoubleCategoryBasics. Require Import UniMath.Bicategories.DoubleCategories.Core.DoubleCats. Require Import UniMath.Bicategories.DoubleCategories.DerivedLaws.TransportLaws. Require Import UniMath.Bicategories.DoubleCategories.Underlying.HorizontalBicategory.