Commit 2020-06-29 03:20 d2b46abb

View on Github →

chore(category_theory/punit): use discrete punit instead of punit (#3201) Analogous to #3191 for punit. I also removed some simp lemmas which can be generated instead by [simps].

Estimated changes

Modified src/algebra/homology/chain_complex.lean

Modified src/category_theory/comma.lean

deleted theorem category_theory.arrow.hom_mk'_left

deleted theorem category_theory.arrow.hom_mk'_right

deleted theorem category_theory.arrow.hom_mk_left

deleted theorem category_theory.arrow.hom_mk_right

deleted theorem category_theory.arrow.mk_hom

deleted theorem category_theory.comma.fst_map

deleted theorem category_theory.comma.fst_obj

deleted theorem category_theory.comma.map_left_comp_hom_app_left

deleted theorem category_theory.comma.map_left_comp_hom_app_right

deleted theorem category_theory.comma.map_left_comp_inv_app_left

deleted theorem category_theory.comma.map_left_comp_inv_app_right

deleted theorem category_theory.comma.map_left_id_hom_app_left

deleted theorem category_theory.comma.map_left_id_hom_app_right

deleted theorem category_theory.comma.map_left_id_inv_app_left

deleted theorem category_theory.comma.map_left_id_inv_app_right

deleted theorem category_theory.comma.map_left_map_left

deleted theorem category_theory.comma.map_left_map_right

deleted theorem category_theory.comma.map_left_obj_hom

deleted theorem category_theory.comma.map_left_obj_left

deleted theorem category_theory.comma.map_left_obj_right

deleted theorem category_theory.comma.map_right_comp_hom_app_left

deleted theorem category_theory.comma.map_right_comp_hom_app_right

deleted theorem category_theory.comma.map_right_comp_inv_app_left

deleted theorem category_theory.comma.map_right_comp_inv_app_right

deleted theorem category_theory.comma.map_right_id_hom_app_left

deleted theorem category_theory.comma.map_right_id_hom_app_right

deleted theorem category_theory.comma.map_right_id_inv_app_left

deleted theorem category_theory.comma.map_right_id_inv_app_right

deleted theorem category_theory.comma.map_right_map_left

deleted theorem category_theory.comma.map_right_map_right

deleted theorem category_theory.comma.map_right_obj_hom

deleted theorem category_theory.comma.map_right_obj_left

deleted theorem category_theory.comma.map_right_obj_right

deleted theorem category_theory.comma.snd_map

deleted theorem category_theory.comma.snd_obj

deleted theorem category_theory.over.hom_mk_left

modified def category_theory.over.map

deleted theorem category_theory.over.over_morphism_right

modified def category_theory.over

deleted theorem category_theory.under.hom_mk_right

modified def category_theory.under.map

deleted theorem category_theory.under.mk_hom

deleted theorem category_theory.under.mk_right

deleted theorem category_theory.under.under_morphism_left

modified def category_theory.under

Modified src/category_theory/connected.lean

added def category_theory.discrete_connected_equiv_punit

Modified src/category_theory/discrete_category.lean

added def category_theory.discrete.equiv_of_equivalence

Modified src/category_theory/elements.lean

modified def category_theory.category_of_elements.comma_equivalence

added theorem category_theory.category_of_elements.comma_equivalence_functor

added theorem category_theory.category_of_elements.comma_equivalence_inverse

modified def category_theory.category_of_elements.from_comma

modified def category_theory.category_of_elements.to_comma

deleted theorem category_theory.category_of_elements.π_map

deleted theorem category_theory.category_of_elements.π_obj

Modified src/category_theory/groupoid.lean

Modified src/category_theory/limits/shapes/zero.lean

Modified src/category_theory/punit.lean

added def category_theory.functor.equiv

added def category_theory.functor.from_punit

added theorem category_theory.functor.punit_ext'

added def category_theory.functor.punit_ext

modified def category_theory.functor.star

deleted theorem category_theory.functor.star_map

deleted theorem category_theory.functor.star_obj