Commit 2020-07-14 14:05 02f2f947

View on Github →

refactor(category_theory/finite_limits): missing piece of #3320 (#3400) A recent PR #3320 did some refactoring of special shapes of limits. It seems I forgot to include wide_pullbacks in that refactor, so I've done that here.

Estimated changes

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

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

added def category_theory.limits.wide_pullback_shape.diagram_iso_wide_cospan

added inductive category_theory.limits.wide_pullback_shape.hom

added theorem category_theory.limits.wide_pullback_shape.hom_id

added def category_theory.limits.wide_pullback_shape.wide_cospan

added def category_theory.limits.wide_pullback_shape

added def category_theory.limits.wide_pushout_shape.diagram_iso_wide_span

added inductive category_theory.limits.wide_pushout_shape.hom

added theorem category_theory.limits.wide_pushout_shape.hom_id

added def category_theory.limits.wide_pushout_shape.wide_span

added def category_theory.limits.wide_pushout_shape

deleted def wide_pullback_shape.diagram_iso_wide_cospan

deleted inductive wide_pullback_shape.hom

deleted theorem wide_pullback_shape.hom_id

deleted def wide_pullback_shape.wide_cospan

deleted def wide_pullback_shape

deleted def wide_pushout_shape.diagram_iso_wide_span

deleted inductive wide_pushout_shape.hom

deleted theorem wide_pushout_shape.hom_id

deleted def wide_pushout_shape.wide_span

deleted def wide_pushout_shape