Theorems · Theorem · category theory

CategoryTheory.Over.hasLimit_of_hasLimit_liftFromOver

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} (F : CategoryTheory.Functor J (CategoryTheory.Over X))
  [CategoryTheory.Limits.HasLimit (CategoryTheory.WithTerminal.liftFromOver.obj F)], CategoryTheory.Limits.HasLimit F

Defined in

Mathlib.CategoryTheory.WithTerminal.Cone

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasLimit