∀ {J : Type u_1} (J' : Type u_2) (h : J ≃ J'),
  (CategoryTheory.Functor.id (CategoryTheory.Limits.WidePullbackShape J)).obj none =
    ((CategoryTheory.Limits.WidePullbackShape.wideCospan none (fun j => some (h j)) fun j =>
              CategoryTheory.Limits.WidePullbackShape.Hom.term (h j)).comp
          (CategoryTheory.Limits.WidePullbackShape.wideCospan none (fun j => some (h.invFun j)) fun j =>
            CategoryTheory.Limits.WidePullbackShape.Hom.term (h.invFun j))).obj
      none