∀ {J : Type u_1} (x : CategoryTheory.Limits.WidePullbackShape J),
  CategoryTheory.WithTerminal.widePullbackShapeEquivObj✝ x =
    match x with
    | some x => CategoryTheory.WithTerminal.of { as := x }
    | none => CategoryTheory.WithTerminal.star