Connected limits in the over category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Shows that the forgetful functor
over B ⥤ C creates connected limits, in particular
over B has
any connected limit which
(Impl) Given a diagram in the over category, produce a natural transformation from the
diagram legs to the specific object.
(Impl) Given a cone in the base category, raise it to a cone in the over category. Note this is
where the connected assumption is used.
(Impl) Show that the raised cone is a limit.
The forgetful functor from the over category creates any connected limit.
The over category has any connected limit which the original category has.