Theorems · Theorem · category theory

CategoryTheory.IsSifted.isSiftedOrEmpty_of_colim_preservesBinaryProducts

∀ (C : Type u) [inst : CategoryTheory.SmallCategory C]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
      CategoryTheory.Limits.colim],
  CategoryTheory.IsSiftedOrEmpty C

If the colim functor (C ⥤ Type) ⥤ Type preserves binary products, then C is sifted or empty.

Defined in

Mathlib.CategoryTheory.Limits.Sifted

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategoryCategoryTheory.Limits.PreservesLimitsOfShape