Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-17 22:00 8b6901b6

View on Github →

Revert "feat(category_theory/limits): is_bilimit" This reverts commit 8edfa75d79ad70c88dbae01ab6166dd8b1fd2ba0.

Estimated changes

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

deleted structure category_theory.limits.bicone.is_bilimit

deleted def category_theory.limits.bicone.of_colimit_cocone

deleted def category_theory.limits.bicone.of_limit_cone

deleted def category_theory.limits.bicone.to_binary_bicone_is_bilimit

modified def category_theory.limits.bicone.to_binary_bicone_is_colimit

modified def category_theory.limits.bicone.to_binary_bicone_is_limit

deleted theorem category_theory.limits.bicone.ι_of_is_limit

deleted theorem category_theory.limits.bicone.π_of_is_colimit

modified theorem category_theory.limits.bicone_ι_π_ne

deleted structure category_theory.limits.binary_bicone.is_bilimit

deleted def category_theory.limits.binary_bicone.to_bicone

deleted def category_theory.limits.binary_bicone.to_bicone_is_bilimit

deleted def category_theory.limits.binary_bicone.to_bicone_is_colimit

deleted def category_theory.limits.binary_bicone.to_bicone_is_limit

deleted def category_theory.limits.binary_biproduct.is_bilimit

deleted def category_theory.limits.biproduct.is_bilimit