Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-27 14:37 92e9d64c

View on Github →

feat(category_theory): restating functor.map and nat_trans.app (#268)

Estimated changes

Modified category_theory/functor.lean

deleted theorem category_theory.functor.coe_def

modified theorem category_theory.functor.comp_map

added def category_theory.functor.map

added theorem category_theory.functor.map_comp_lemma

added theorem category_theory.functor.map_id_lemma

added theorem category_theory.functor.mk_map

added theorem category_theory.functor.mk_obj

Modified category_theory/functor_category.lean

modified theorem category_theory.functor.category.comp_app

modified theorem category_theory.functor.category.nat_trans.app_naturality

modified theorem category_theory.functor.category.nat_trans.naturality_app

Modified category_theory/natural_transformation.lean

deleted theorem category_theory.nat_trans.coe_def

modified theorem category_theory.nat_trans.exchange

modified theorem category_theory.nat_trans.hcomp_app

added theorem category_theory.nat_trans.mk_app

added theorem category_theory.nat_trans.naturality_lemma

modified theorem category_theory.nat_trans.vcomp_assoc

Modified category_theory/opposites.lean

Modified category_theory/products.lean

Modified category_theory/types.lean