∀ {B : Type u_1} [inst : Quiver B] {a b c d : CategoryTheory.FreeBicategory B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c)
  (h : c ⟶ d),
  Quot.map (CategoryTheory.FreeBicategory.Hom₂.whisker_right (CategoryTheory.CategoryStruct.comp g h)) ⋯ η =
    CategoryTheory.CategoryStruct.comp
      { hom := Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator f g h),
          inv := Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h),
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.inv
      (CategoryTheory.CategoryStruct.comp
        (Quot.map (CategoryTheory.FreeBicategory.Hom₂.whisker_right h) ⋯
          (Quot.map (CategoryTheory.FreeBicategory.Hom₂.whisker_right g) ⋯ η))
        { hom := Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator f' g h),
            inv := Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.associator_inv f' g h),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom)