Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-09-01 11:29 6d2b3ed8

View on Github →

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

Estimated changes

Modified src/category_theory/adjunction/basic.lean

modified def category_theory.adjunction.id

Modified src/category_theory/comma.lean

modified def category_theory.comma.map_left_id

modified def category_theory.comma.map_right_id

modified def category_theory.over

modified def category_theory.under

Modified src/category_theory/equivalence.lean

modified def category_theory.functor.fun_inv_id

modified def category_theory.functor.inv_fun_id

Modified src/category_theory/fully_faithful.lean

Modified src/category_theory/functor.lean

modified theorem category_theory.functor.id_map

modified theorem category_theory.functor.id_obj

Modified src/category_theory/limits/cones.lean

modified def category_theory.limits.cocones.precompose_id

modified def category_theory.limits.cones.postcompose_id

Modified src/category_theory/limits/limits.lean

Modified src/category_theory/limits/preserves.lean

Modified src/category_theory/monad/adjunction.lean

modified theorem category_theory.adjunction.monad_η_app

modified theorem category_theory.adjunction.monad_μ_app

modified theorem category_theory.monad.comparison_map_f

modified theorem category_theory.monad.comparison_obj_a

Modified src/category_theory/monad/basic.lean

Modified src/category_theory/monoidal/category.lean

Modified src/category_theory/monoidal/functor.lean

Modified src/category_theory/natural_isomorphism.lean

modified def category_theory.functor.ulift_down_up

modified def category_theory.functor.ulift_up_down

Modified src/category_theory/products/default.lean

modified def category_theory.prod.symmetry

Modified src/category_theory/whiskering.lean

modified def category_theory.functor.left_unitor

modified def category_theory.functor.right_unitor

Modified src/category_theory/yoneda.lean

Modified src/topology/Top/opens.lean

modified def topological_space.opens.map_id