∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  CategoryTheory.Bicategory.whiskerRight η h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp f h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h)
        (CategoryTheory.Iso.refl (CategoryTheory.CategoryStruct.comp g h)).hom)