If colimits of shape K commute with finite limits, then K is filtered. #
theorem
CategoryTheory.isFiltered_of_nonempty_limit_colimit_to_colimit_limit
{K : Type v}
[SmallCategory K]
(h :
∀ {J : Type v} [inst : SmallCategory J] [FinCategory J] (F : Functor J (Functor K (Type v))),
Nonempty (Limits.limit (Limits.colimit F.flip) ⟶ Limits.colimit (Limits.limit F)))
:
A converse to colimitLimitIso: if colimits of shape K commute with finite
limits, then K is filtered.