Theorems · Theorem · category theory

CategoryTheory.Limits.ReflectsColimit.reflects

∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {J : Type w} {inst_2 : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsColimit K F]
  {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit (F.mapCocone c)),
  Nonempty (CategoryTheory.Limits.IsColimit c)

Defined in

Mathlib.CategoryTheory.Limits.Preserves.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Limits.ReflectsColimit