Commit 2020-08-28 07:24 ceacf541

View on Github →

feat(category_theory/filtered): filtered categories, and filtered colimits in Type (#3960) This is some work @rwbarton did last year. I've merged master, written some comments, and satisfied the linter.

Estimated changes

Created src/category_theory/filtered.lean

Modified src/category_theory/limits/types.lean

added theorem category_theory.limits.types.filtered_colimit.colimit_eq_iff

added theorem category_theory.limits.types.filtered_colimit.is_colimit_eq_iff

added theorem category_theory.limits.types.jointly_surjective

added theorem category_theory.limits.types.ι_desc_apply

Modified src/data/quot.lean

added theorem quot.eq