∀ (B : Type u_2) [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
  (CategoryTheory.StrictlyUnitaryPseudofunctor.id B).map (CategoryTheory.CategoryStruct.comp f g) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.StrictlyUnitaryPseudofunctor.id B).map f)
      ((CategoryTheory.StrictlyUnitaryPseudofunctor.id B).map g)