∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_2} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  (s : CategoryTheory.Limits.WidePullbackCone f) {ι' : Type u_3} (e : ι' ≃ ι), (s.reindex e).base = s.base