Commit 2026-09-28 03:52 913e6df6

View on Github →

chore(CategoryTheory/Limits/Shapes/WidePullBacks): use to_dual (#42794) Use to_dual for wide pullbacks/pushouts. Additionally:

Tag WidePullbackShape.mkCone with implicit_reducible and remove some backward options.

Estimated changes

Modified Mathlib/AlgebraicTopology/CechNerve.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

deleted theorem CategoryTheory.Limits.WidePushout.arrow_ι

deleted theorem CategoryTheory.Limits.WidePushout.eq_desc_of_comp_eq

deleted theorem CategoryTheory.Limits.WidePushout.head_desc

deleted theorem CategoryTheory.Limits.WidePushout.hom_eq_desc

deleted theorem CategoryTheory.Limits.WidePushout.hom_ext

deleted theorem CategoryTheory.Limits.WidePushout.ι_desc

modified inductive CategoryTheory.Limits.WidePushoutShape.Hom

deleted def CategoryTheory.Limits.WidePushoutShape.diagramIsoWideSpan

deleted def CategoryTheory.Limits.WidePushoutShape.equivalenceOfEquiv

deleted theorem CategoryTheory.Limits.WidePushoutShape.hom_id

deleted def CategoryTheory.Limits.WidePushoutShape.mkCocone

deleted def CategoryTheory.Limits.WidePushoutShape.uliftEquivalence

deleted def CategoryTheory.Limits.WidePushoutShape.wideSpan

deleted def CategoryTheory.Limits.WidePushoutShape

deleted theorem CategoryTheory.Limits.hasWidePullbacks_shrink

deleted def CategoryTheory.Limits.widePullbackShapeOpEquiv

deleted def CategoryTheory.Limits.widePullbackShapeOpUnop

deleted def CategoryTheory.Limits.widePullbackShapeUnopOp

deleted def CategoryTheory.Limits.widePushoutShapeOp

deleted def CategoryTheory.Limits.widePushoutShapeOpMap

deleted def CategoryTheory.Limits.widePushoutShapeUnop