∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {C : Type u_5} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {X Y : F ⟶ G} (f : CategoryTheory.Pseudofunctor.StrongTrans.Hom X Y),
  { as := f.as.vcomp { as := CategoryTheory.Pseudofunctor.StrongTrans.Modification.id Y }.as } = f