∀ {B : Type u_1} {C : Type u_2} [inst : CategoryTheory.Bicategory C] {F : B → C}
  {a b : CategoryTheory.Bicategory.InducedBicategory C F} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.Bicategory.InducedBicategory.mkHom₂
      (CategoryTheory.Bicategory.whiskerRight η.hom (CategoryTheory.CategoryStruct.id b).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.InducedBicategory.isoMk (CategoryTheory.Bicategory.rightUnitor f.hom)).hom
      (CategoryTheory.CategoryStruct.comp η
        (CategoryTheory.Bicategory.InducedBicategory.isoMk (CategoryTheory.Bicategory.rightUnitor g.hom)).inv)