∀ (B : Type u_2) [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b),
  (CategoryTheory.PrelaxFunctor.id B).map₂ (CategoryTheory.Bicategory.rightUnitor f).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.rightUnitor ((CategoryTheory.PrelaxFunctor.id B).map f)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft ((CategoryTheory.PrelaxFunctor.id B).map f)
          (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id b)))
        (CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b))))