mathlib3

6d2b3ed8 - chore(category_theory/notation): consistently use notation for functor.id (#1378)

chore(category_theory/notation): consistently use notation for functor.id (#1378) * chore(category_theory/notation): consistently use notation for functor.id * oops, overzealous search-and-replace * more * more * more