∀ {a b c : CategoryTheory.Cat} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c),
  CategoryTheory.WithInitial.prelaxfunctor.map₂ (CategoryTheory.Bicategory.whiskerRight η h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithInitial.mapComp f.toFunctor h.toFunctor)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.WithInitial.prelaxfunctor.map₂ η)
          (CategoryTheory.WithInitial.prelaxfunctor.map h))
        (CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithInitial.mapComp g.toFunctor h.toFunctor)).inv)