Theorems · Definition · category theory

CategoryTheory.Functor.Initial.isLimitExtendConeEquiv

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Initial] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  (t : CategoryTheory.Limits.Cone (F.comp G)) →
                    CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.Initial.extendCone.obj t) ≃
                      CategoryTheory.Limits.IsLimit t

When F is initial, and t : Cone (F ⋙ G), extendCone.obj t is a limit cone exactly when t is.

Defined in

Mathlib.CategoryTheory.Limits.Final

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.InitialCategoryTheory.Category