∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] {X Y : CategoryTheory.Cat} (F : X ⟶ Y)
  {X_1 Y_1 : CategoryTheory.Join (↑X) D} (f : X_1 ⟶ Y_1),
  ((CategoryTheory.Join.pseudofunctorLeft D).map F).toFunctor.map f =
    CategoryTheory.Join.homInduction (fun x x_1 f => (CategoryTheory.Join.inclLeft (↑Y) D).map (F.toFunctor.map f))
      (fun x x_1 g => (CategoryTheory.Join.inclRight (↑Y) D).map g)
      (fun c d => CategoryTheory.Join.edge (F.toFunctor.obj c) d) f