English
The functor to another CompHausLike preserves pullbacks if they exist.
Русский
Функтор к другой CompHausLike сохраняет пуллбэки, если они существуют.
LaTeX
$$$\\text{PreservesLimit}(\\mathrm{cospan} f g)\\; (\\mathrm{toCompHausLike}\, h)$$$
Lean4
/-- The functor to `TopCat` preserves finite coproducts if they exist. -/
instance (P) [HasExplicitFiniteCoproducts.{0} P] : PreservesFiniteCoproducts (compHausLikeToTop P) :=
by
refine ⟨fun _ ↦ ⟨fun {F} ↦ ?_⟩⟩
suffices PreservesColimit (Discrete.functor (F.obj ∘ Discrete.mk)) (compHausLikeToTop P) from
preservesColimit_of_iso_diagram _ Discrete.natIsoFunctor.symm
apply preservesColimit_of_preserves_colimit_cocone (CompHausLike.finiteCoproduct.isColimit _)
exact TopCat.sigmaCofanIsColimit _
