Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-07 17:54 851e83ec

View on Github →

feat(category_theory): colimits for pi categories (#4054)

Estimated changes

Modified src/category_theory/limits/pi.lean

added def category_theory.pi.cocone_comp_eval

added def category_theory.pi.cocone_of_cocone_comp_eval

added def category_theory.pi.cocone_of_cocone_eval_is_colimit

added def category_theory.pi.has_colimit_of_has_colimit_comp_eval