Commit 2026-01-30 11:40 1f2089e0

View on Github →

chore(CategoryTheory): dualize NatTrans.Equifibered (#34343) ... and move to a new file.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/Pullback/Equifibered.lean

added theorem CategoryTheory.NatTrans.Coequifibered.comp

added theorem CategoryTheory.NatTrans.Coequifibered.of_discrete

added theorem CategoryTheory.NatTrans.Coequifibered.op

added theorem CategoryTheory.NatTrans.Coequifibered.unop

added theorem CategoryTheory.NatTrans.Coequifibered.whiskerLeft

added theorem CategoryTheory.NatTrans.Coequifibered.whiskerRight

added def CategoryTheory.NatTrans.Coequifibered

added theorem CategoryTheory.NatTrans.Coequifibered_of_isIso

added theorem CategoryTheory.NatTrans.Equifibered.comp

added theorem CategoryTheory.NatTrans.Equifibered.of_discrete

added theorem CategoryTheory.NatTrans.Equifibered.op

added theorem CategoryTheory.NatTrans.Equifibered.unop

added theorem CategoryTheory.NatTrans.Equifibered.whiskerLeft

added theorem CategoryTheory.NatTrans.Equifibered.whiskerRight

added def CategoryTheory.NatTrans.Equifibered

added theorem CategoryTheory.NatTrans.equifibered_of_isIso

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

deleted theorem CategoryTheory.NatTrans.Equifibered.comp

deleted theorem CategoryTheory.NatTrans.Equifibered.whiskerLeft

deleted theorem CategoryTheory.NatTrans.Equifibered.whiskerRight

deleted def CategoryTheory.NatTrans.Equifibered

deleted theorem CategoryTheory.NatTrans.equifibered_of_discrete

deleted theorem CategoryTheory.NatTrans.equifibered_of_isIso

deleted theorem CategoryTheory.mapPair_equifibered