Lean4
/-- A choice of limit cone for a functor `F : J ⥤ TopCat`.
Generally you should just use `limit.cone F`, unless you need the actual definition
(which is in terms of `Types.limitCone`).
-/
def limitCone (F : J ⥤ TopCat.{max v u}) : Cone F
where
pt := TopCat.of {u : ∀ j : J, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j}
π :=
{ app := fun j =>
ofHom
{ toFun := fun u => u.val j
continuous_toFun := Continuous.comp (continuous_apply _) (continuous_subtype_val) }
naturality := fun X Y f => by
ext a
exact (a.2 f).symm }