∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {g : a ⟶ c} {h : b ⟶ d} {l₁ l₂ : a ⟶ b} {l₃ : c ⟶ d}
  (α : l₂ ⟶ l₁) (β : CategoryTheory.CategoryStruct.comp g l₃ ⟶ CategoryTheory.CategoryStruct.comp l₂ h),
  CategoryTheory.Bicategory.leftAdjointConjugateSquare.vcomp α β =
    CategoryTheory.CategoryStruct.comp β (CategoryTheory.Bicategory.whiskerRight α h)