Commit 2020-05-29 16:24 77674a04

View on Github →

chore(category_theory): T50000 challenge (#2840) A lame effort at making something compile with -T50000. No actual speed improvement, just split up a definition into pieces.

Estimated changes

Modified src/category_theory/limits/over.lean

added def category_theory.over.construct_products.cones_equiv_counit_iso

added def category_theory.over.construct_products.cones_equiv_inverse_obj

added def category_theory.over.construct_products.cones_equiv_unit_iso

Modified src/category_theory/limits/shapes/binary_products.lean