Documentation

Mathlib.CategoryTheory.Limits.Constructions.Over.Connected

Connected limits in the over category #

Shows that the forgetful functor Over B ⥤ C creates connected limits, in particular Over B has any connected limit which C has.

(Impl) Given a diagram in the over category, produce a natural transformation from the diagram legs to the specific object.

Instances For

    (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.

    Instances For