Theorems · Definition · category theory

CategoryTheory.WithTerminal.isLimitEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{w', w} J] →
        {X : C} →
          {K : CategoryTheory.Functor J (CategoryTheory.Over X)} →
            {t : CategoryTheory.Limits.Cone K} →
              CategoryTheory.Limits.IsLimit (CategoryTheory.WithTerminal.coneEquiv.functor.obj t) ≃
                CategoryTheory.Limits.IsLimit t

A cone t of K : J ⥤ Over X is a limit if and only if the corresponding cone coneLift t of liftFromOver.obj K : WithTerminal K ⥤ C is a limit.

Defined in

Mathlib.CategoryTheory.WithTerminal.Cone

Cited by

3 results in Mathlib

Foundations

Depth 46 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Category