Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-12-18 00:48 3d4297b3

View on Github →

feat(category_theory/eq_to_hom): equality of functors; more simp lemmas (#526)

Estimated changes

Created category_theory/eq_to_hom.lean

added def category_theory.eq_to_hom

added theorem category_theory.eq_to_hom_app

added theorem category_theory.eq_to_hom_map

added theorem category_theory.eq_to_hom_refl

added theorem category_theory.eq_to_hom_trans

added theorem category_theory.eq_to_hom_trans_assoc

added theorem category_theory.eq_to_iso.hom

added def category_theory.eq_to_iso

added theorem category_theory.eq_to_iso_map

added theorem category_theory.eq_to_iso_refl

added theorem category_theory.eq_to_iso_trans

added theorem category_theory.functor.congr_hom

added theorem category_theory.functor.congr_obj

added theorem category_theory.functor.ext

Modified category_theory/examples/topological_spaces.lean

Modified category_theory/isomorphism.lean

deleted def category_theory.eq_to_hom

deleted theorem category_theory.eq_to_hom_refl

deleted theorem category_theory.eq_to_hom_trans

deleted theorem category_theory.eq_to_iso.hom

deleted def category_theory.eq_to_iso

deleted theorem category_theory.eq_to_iso_refl

deleted theorem category_theory.eq_to_iso_trans

deleted theorem category_theory.functor.eq_to_iso