Commit 2020-05-20 15:34 164c2e3c

View on Github →

chore(category_theory): attributes and a transport proof (#2751) A couple of cleanups, modified a proof or two so that @[simps] can be used, which let me clean up some other proofs. Also a proof that we can transfer that F preserves the limit K along an isomorphism in K. (Preparation for some PRs from my topos project)

Estimated changes

Modified src/category_theory/equivalence.lean

modified def category_theory.equivalence.refl

modified def category_theory.equivalence.symm

Modified src/category_theory/limits/cones.lean

Modified src/category_theory/limits/preserves.lean

added def category_theory.limits.preserves_limit_of_iso

Modified src/category_theory/natural_isomorphism.lean

modified theorem category_theory.nat_iso.hom_inv_id_app

modified theorem category_theory.nat_iso.inv_hom_id_app

modified theorem category_theory.nat_iso.of_components.app

modified theorem category_theory.nat_iso.of_components.hom_app

modified theorem category_theory.nat_iso.of_components.inv_app

modified def category_theory.nat_iso.of_components