mathlib

77674a04 - chore(category_theory): T50000 challenge (#2840)

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. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>