Theorems · Definition · category theory

CategoryTheory.Limits.isLimitEquivIsTerminalOfIsEmpty

(C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
        [IsEmpty J] →
          {F : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.Cone F) → CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsTerminal c.pt

If F is an empty diagram, then a cone over F is limiting iff the cone point is terminal.

Defined in

Mathlib.CategoryTheory.Limits.Shapes.IsTerminal

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryIsEmpty