Commit 2020-08-17 04:44 6773f526

View on Github →

feat(category_theory): limits in the category of indexed families (#3737) A continuation of #3735, hopefully useful in #3638.

Estimated changes

Created src/category_theory/limits/pi.lean

added def category_theory.pi.cone_comp_eval

added def category_theory.pi.cone_of_cone_comp_eval

added def category_theory.pi.cone_of_cone_eval_is_limit

added def category_theory.pi.has_limit_of_has_limit_comp_eval

Modified src/category_theory/pi/basic.lean

added def category_theory.pi'