Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-14 01:59 ade1ee30

View on Github →

feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y) (#2139)

feat(category_theory/limits): derive has_binary_products from has_limit (pair X Y)
Rename of_diagram to diagram_iso

Estimated changes

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

added def category_theory.limits.diagram_iso_pair

added def category_theory.limits.has_binary_coproducts_of_has_colimit_pair

added def category_theory.limits.has_binary_products_of_has_limit_pair

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

added def category_theory.limits.diagram_iso_parallel_pair

added def category_theory.limits.has_coequalizers_of_has_colimit_parallel_pair

added def category_theory.limits.has_equalizers_of_has_limit_parallel_pair

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

added def category_theory.limits.diagram_iso_cospan

added def category_theory.limits.diagram_iso_span

added def category_theory.limits.has_pullbacks_of_has_limit_cospan

added def category_theory.limits.has_pushouts_of_has_colimit_span