∀ {B : Type u_1} [inst : Quiver B] {a b c d : CategoryTheory.FreeBicategory B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g')
  (h : c ⟶ d),
  Quot.map (CategoryTheory.FreeBicategory.Hom₂.whisker_right h) ⋯
      (Quot.map (CategoryTheory.FreeBicategory.Hom₂.whisker_left f) ⋯ η) =
    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 := ⋯ }.hom
      (CategoryTheory.CategoryStruct.comp
        (Quot.map (CategoryTheory.FreeBicategory.Hom₂.whisker_left f) ⋯
          (Quot.map (CategoryTheory.FreeBicategory.Hom₂.whisker_right h) ⋯ η))
        { 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)