Commit 2020-07-14 11:42 a0846da1

chore(category_theory/limits/over): split a slow file (#3399) This was previously the last file to finish compiling when compiling category_theory/. This PR splits it into some smaller pieces which can compile in parallel (and some pieces now come earlier in the import hierarchy). No change to content.