mathlib

c68f23df - chore(category_theory/types): add documentation, remove bad simp lemmas and instances, add notation for functions as morphisms (#2383)

chore(category_theory/types): add documentation, remove bad simp lemmas and instances, add notation for functions as morphisms (#2383) * Add module doc and doc strings for `src/category_theory/types.lean`. * Remove some bad simp lemmas and instances in that file and `src/category_theory/category/default.lean`. * Add a notation `↾f` which enables Lean to see a function `f : α → β` as a morphism `α ⟶ β` in the category of types.