Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.Comma.hasLimit_of_closedUnderLimitsOfShape

∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P : CategoryTheory.MorphismProperty T) {A : Type u_2}
  {B : Type u_3} {J : Type u_4} [inst_1 : CategoryTheory.Category.{v_2, u_2} A]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} B] [inst_3 : CategoryTheory.Category.{v_4, u_4} J]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (D : CategoryTheory.Functor J (CategoryTheory.MorphismProperty.Comma L R P ⊤ ⊤))
  [(CategoryTheory.MorphismProperty.commaObj L R P).IsClosedUnderLimitsOfShape J]
  [CategoryTheory.Limits.HasLimit (D.comp (CategoryTheory.MorphismProperty.Comma.forget L R P ⊤ ⊤))],
  CategoryTheory.Limits.HasLimit D

Defined in

Mathlib.CategoryTheory.Limits.MorphismProperty

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShapeCategoryTheory.Limits.HasLimit