Commit 2022-09-30 23:37 e4ee4e30
View on Github →feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373) We will use this in the future to show that if C has finite colimits, then Ind(C) is cocomplete.
feat(category_theory/limits): colimits from finite colimits and filtered colimits (#16373) We will use this in the future to show that if C has finite colimits, then Ind(C) is cocomplete.