Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-10 07:17 89924726

View on Github →

fix(category_theory): make the nat_trans arrow ⟹ a synonym for the hom arrow (#907)

removing the nat_trans and vcomp notations; use \hom and \gg
a simpler proposal
getting rid of vcomp
fix
update notations in documentation
typo in docs

Estimated changes

Modified docs/theories/category_theory.md

Modified src/category_theory/adjunction.lean

Modified src/category_theory/comma.lean

modified def category_theory.comma.map_left

modified def category_theory.comma.map_left_comp

modified def category_theory.comma.map_right

modified def category_theory.comma.map_right_comp

modified def category_theory.comma.nat_trans

Modified src/category_theory/discrete_category.lean

Modified src/category_theory/eq_to_hom.lean

Modified src/category_theory/functor_category.lean

modified theorem category_theory.functor.category.id_app

modified theorem category_theory.functor.category.nat_trans.app_naturality

modified theorem category_theory.functor.category.nat_trans.naturality_app

Modified src/category_theory/limits/cones.lean

modified theorem category_theory.functor.cocones_obj

Modified src/category_theory/limits/limits.lean

modified def category_theory.limits.is_colimit.hom_iso

modified def category_theory.limits.is_limit.hom_iso

Modified src/category_theory/limits/types.lean

modified theorem category_theory.limits.types.types_colimit_map

modified theorem category_theory.limits.types.types_limit_map

Modified src/category_theory/natural_isomorphism.lean

deleted theorem category_theory.nat_iso.hom_vcomp_inv

deleted theorem category_theory.nat_iso.inv_vcomp_hom

Modified src/category_theory/natural_transformation.lean

modified theorem category_theory.nat_trans.congr_app

modified theorem category_theory.nat_trans.exchange

modified theorem category_theory.nat_trans.ext

modified def category_theory.nat_trans.hcomp

modified theorem category_theory.nat_trans.hcomp_app

modified def category_theory.nat_trans.vcomp

modified theorem category_theory.nat_trans.vcomp_app

modified theorem category_theory.nat_trans.vcomp_assoc

Modified src/category_theory/products.lean

modified def category_theory.nat_trans.prod

modified theorem category_theory.nat_trans.prod_app

Modified src/category_theory/types.lean

added theorem category_theory.functor_to_types.comp

deleted theorem category_theory.functor_to_types.vcomp

Modified src/category_theory/whiskering.lean

modified theorem category_theory.whisker_left.app

modified def category_theory.whisker_left

added theorem category_theory.whisker_left_comp

modified theorem category_theory.whisker_left_twice

deleted theorem category_theory.whisker_left_vcomp

modified theorem category_theory.whisker_right.app

modified def category_theory.whisker_right

added theorem category_theory.whisker_right_comp

modified theorem category_theory.whisker_right_left

modified theorem category_theory.whisker_right_twice

deleted theorem category_theory.whisker_right_vcomp

modified theorem category_theory.whiskering_left_map_app_app

modified theorem category_theory.whiskering_left_obj_map

modified theorem category_theory.whiskering_right_map_app_app

modified theorem category_theory.whiskering_right_obj_map

Modified src/category_theory/yoneda.lean

modified def category_theory.yoneda_sections

modified def category_theory.yoneda_sections_small