Commit 2020-03-11 10:15 43431be5

View on Github →

chore(category_theory): remove functor.of (#2127)

chore(category_theory): remove functor.of
fix

Estimated changes

Modified src/category_theory/comma.lean

modified def category_theory.over.map

modified def category_theory.over

modified def category_theory.under.map

modified def category_theory.under

Modified src/category_theory/elements.lean

modified def category_theory.category_of_elements.comma_equivalence

modified def category_theory.category_of_elements.from_comma

modified def category_theory.category_of_elements.to_comma

Modified src/category_theory/punit.lean

deleted theorem category_theory.functor.of.map_app

deleted theorem category_theory.functor.of.obj_map

deleted theorem category_theory.functor.of.obj_obj

deleted def category_theory.functor.of