∀ (B : Type u_1) [inst : Quiver B] {a b c : CategoryTheory.LocallyDiscrete (CategoryTheory.Paths B)} (f : a ⟶ b)
  {g h : b ⟶ c} (η : g ⟶ h),
  (CategoryTheory.FreeBicategory.preinclusion B).map₂ (CategoryTheory.Bicategory.whiskerLeft f η) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.FreeBicategory.inclusionMapCompAux f.as g.as).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft ((CategoryTheory.FreeBicategory.preinclusion B).map f)
          ((CategoryTheory.FreeBicategory.preinclusion B).map₂ η))
        (CategoryTheory.FreeBicategory.inclusionMapCompAux f.as h.as).inv)