∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {toFunctor : CategoryTheory.Functor 𝒳.obj 𝒴.obj}
  {w : autoParam (toFunctor.comp 𝒴.p = 𝒳.p) CategoryTheory.BasedFunctor.w._autoParam}
  {toFunctor_1 : CategoryTheory.Functor 𝒳.obj 𝒴.obj}
  {w_1 : autoParam (toFunctor_1.comp 𝒴.p = 𝒳.p) CategoryTheory.BasedFunctor.w._autoParam},
  { toFunctor := toFunctor, w := w } = { toFunctor := toFunctor_1, w := w_1 } → toFunctor = toFunctor_1