Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-08 10:16 b0564b2b

View on Github →

feat(category_theory): propose removing coercions from category_theory/ (#463)

Estimated changes

Modified category_theory/embedding.lean

modified theorem category_theory.functor.image_preimage

modified def category_theory.functor.preimage

modified def category_theory.preimage_iso

deleted theorem category_theory.preimage_iso_coe

added theorem category_theory.preimage_iso_hom

added theorem category_theory.preimage_iso_inv

deleted theorem category_theory.preimage_iso_symm_coe

Modified category_theory/examples/topological_spaces.lean

modified theorem category_theory.examples.map_id_obj

Modified category_theory/full_subcategory.lean

modified def category_theory.full_subcategory_embedding

Modified category_theory/functor.lean

modified theorem category_theory.functor.comp_obj

modified theorem category_theory.functor.id_obj

deleted def category_theory.functor.map

deleted theorem category_theory.functor.map_comp

deleted theorem category_theory.functor.map_id

deleted theorem category_theory.functor.mk_map

deleted theorem category_theory.functor.mk_obj

deleted theorem category_theory.functor.obj_eq_coe

Modified category_theory/functor_category.lean

modified theorem category_theory.functor.category.comp_app

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 category_theory/isomorphism.lean

modified def category_theory.functor.on_iso

modified theorem category_theory.functor.on_iso_hom

modified theorem category_theory.functor.on_iso_inv

deleted theorem category_theory.iso.hom_eq_coe

deleted theorem category_theory.iso.hom_inv_id

deleted theorem category_theory.iso.inv_eq_coe

deleted theorem category_theory.iso.inv_hom_id

deleted theorem category_theory.iso.refl_coe

added theorem category_theory.iso.refl_hom

added theorem category_theory.iso.refl_inv

modified theorem category_theory.iso.refl_symm

deleted theorem category_theory.iso.refl_symm_coe

added theorem category_theory.iso.symm_hom

added theorem category_theory.iso.symm_inv

deleted theorem category_theory.iso.trans_coe

added theorem category_theory.iso.trans_hom

added theorem category_theory.iso.trans_inv

modified theorem category_theory.iso.trans_symm

deleted theorem category_theory.iso.trans_symm_coe

Modified category_theory/natural_isomorphism.lean

modified def category_theory.functor.assoc

modified def category_theory.functor.comp_id

modified def category_theory.functor.id_comp

modified def category_theory.nat_iso.app

added theorem category_theory.nat_iso.app_hom

added theorem category_theory.nat_iso.app_inv

modified theorem category_theory.nat_iso.comp_app

deleted theorem category_theory.nat_iso.hom_eq_coe

deleted theorem category_theory.nat_iso.inv_eq_symm_coe

deleted theorem category_theory.nat_iso.mk_app'

deleted theorem category_theory.nat_iso.mk_app

modified theorem category_theory.nat_iso.naturality_1

modified theorem category_theory.nat_iso.naturality_2

modified def category_theory.nat_iso.of_components.app

modified def category_theory.nat_iso.of_components.hom_app

modified def category_theory.nat_iso.of_components.inv_app

modified def category_theory.nat_iso.of_components

Modified category_theory/natural_transformation.lean

deleted theorem category_theory.nat_trans.app_eq_coe

modified theorem category_theory.nat_trans.exchange

modified theorem category_theory.nat_trans.ext

modified theorem category_theory.nat_trans.hcomp_app

modified theorem category_theory.nat_trans.id_app

deleted theorem category_theory.nat_trans.mk_app

deleted theorem category_theory.nat_trans.naturality

modified theorem category_theory.nat_trans.vcomp_app

Modified category_theory/opposites.lean

modified theorem category_theory.functor.hom_obj

modified theorem category_theory.functor.opposite_obj

Modified category_theory/products.lean

modified def category_theory.evaluation

modified theorem category_theory.functor.prod_map

modified theorem category_theory.functor.prod_obj

modified theorem category_theory.nat_trans.prod_app

Modified category_theory/types.lean

modified def category_theory.forget

modified theorem category_theory.functor_to_types.hcomp

modified theorem category_theory.functor_to_types.map_comp

modified theorem category_theory.functor_to_types.map_id

modified theorem category_theory.functor_to_types.naturality

modified theorem category_theory.functor_to_types.vcomp

deleted theorem category_theory.types.iso_mk_coe

Modified category_theory/whiskering.lean

modified theorem category_theory.whisker_left.app

modified theorem category_theory.whisker_left_vcomp

modified def category_theory.whisker_right

modified theorem category_theory.whisker_right_vcomp

modified def category_theory.whiskering_left

Modified category_theory/yoneda.lean

modified theorem category_theory.yoneda.map_app

modified theorem category_theory.yoneda.naturality

modified theorem category_theory.yoneda.obj_map

modified theorem category_theory.yoneda.obj_map_id

modified theorem category_theory.yoneda.obj_obj

modified def category_theory.yoneda

modified def category_theory.yoneda_evaluation

modified def category_theory.yoneda_lemma

modified def category_theory.yoneda_pairing

Modified docs/theories/category_theory.md