Commit 2022-04-10 21:57 5bf57407

chore(category_theory/fin_category): Speed up as_type_equiv_obj_as_type (#13298) Rename obj_as_type_equiv_as_type to as_type_equiv_obj_as_type (likely a typo). Use equivalence.mk instead of equivalence.mk' to build it and split the functors to separate definitions to tag them with @[simps] and make dsimp go further. On my machine, this cuts down the compile time from 41s to 3s.