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