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