Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-20 03:59 6c97ce02

View on Github →

feat(category_theory): some natural isomorphisms related to composition by functors (#2189)

feat(category_theory): some natural isomorphisms related to composition by functors
tidy up
cleanup
fix
better design

Estimated changes

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

modified def category_theory.limits.map_pair

added def category_theory.limits.map_pair_iso

modified theorem category_theory.limits.map_pair_left

modified theorem category_theory.limits.map_pair_right

added def category_theory.limits.pair_comp

deleted def category_theory.limits.pair_function

modified theorem category_theory.limits.pair_obj_left

modified theorem category_theory.limits.pair_obj_right

Modified src/category_theory/pempty.lean

added def category_theory.functor.empty_ext