Commit 2026-08-17 12:02 de2aa1f4

View on Github →

chore(CategoryTheory/Limits/Shapes/Terminal): use to_dual (#42842) This PR uses to_dual to generate declarations about Initial and IsInitial from those about Terminal and IsTerminal. CategoryTheory.Limits.initial.to_comp_assoc has been removed, since it is weaker than CategoryTheory.Limits.initial.to_comp.

Estimated changes

Modified Mathlib/CategoryTheory/Category/Preorder.lean

Modified Mathlib/CategoryTheory/Iso.lean

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

deleted def CategoryTheory.Limits.Functor.isInitialConst

deleted theorem CategoryTheory.Limits.Functor.isInitialConst_to_app

deleted theorem CategoryTheory.Limits.IsColimit.isIso_ι_app_of_isTerminal

deleted theorem CategoryTheory.Limits.IsInitial.epi_to

deleted def CategoryTheory.Limits.IsInitial.equivOfIso

deleted theorem CategoryTheory.Limits.IsInitial.hom_ext

deleted theorem CategoryTheory.Limits.IsInitial.isSplitEpi_to

deleted def CategoryTheory.Limits.IsInitial.ofIso

deleted def CategoryTheory.Limits.IsInitial.ofUnique

deleted def CategoryTheory.Limits.IsInitial.ofUniqueHom

deleted def CategoryTheory.Limits.IsInitial.to

deleted theorem CategoryTheory.Limits.IsInitial.to_comp

deleted theorem CategoryTheory.Limits.IsInitial.to_self

deleted def CategoryTheory.Limits.IsInitial.uniqueUpToIso

modified def CategoryTheory.Limits.IsTerminal.ofUnique

modified def CategoryTheory.Limits.IsTerminal.ofUniqueHom

deleted def CategoryTheory.Limits.IsTerminal.op

deleted def CategoryTheory.Limits.IsTerminal.unop

deleted def CategoryTheory.Limits.asEmptyCocone

deleted def CategoryTheory.Limits.coconeOfDiagramInitial

deleted def CategoryTheory.Limits.coconeOfDiagramTerminal

deleted def CategoryTheory.Limits.colimitOfDiagramInitial

deleted def CategoryTheory.Limits.colimitOfDiagramTerminal

deleted def CategoryTheory.Limits.initialOpOfTerminal

deleted def CategoryTheory.Limits.initialUnopOfTerminal

deleted def CategoryTheory.Limits.isColimitChangeEmptyCocone

deleted def CategoryTheory.Limits.isColimitEmptyCoconeEquiv

deleted def CategoryTheory.Limits.isColimitEquivIsInitialOfIsEmpty

deleted def CategoryTheory.Limits.isInitialBot

deleted def CategoryTheory.Limits.isInitialEquivUnique

deleted theorem CategoryTheory.Limits.isIso_of_isInitial

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

deleted theorem CategoryTheory.Limits.IsInitial.hasInitial

deleted theorem CategoryTheory.Limits.hasInitialChangeDiagram

deleted theorem CategoryTheory.Limits.hasInitialChangeUniverse

deleted theorem CategoryTheory.Limits.hasInitial_of_hasTerminal_op

deleted theorem CategoryTheory.Limits.hasInitial_of_unique

deleted theorem CategoryTheory.Limits.initial.hom_ext

deleted theorem CategoryTheory.Limits.initial.to_comp

deleted def CategoryTheory.Limits.initialComparison

deleted def CategoryTheory.Limits.initialIsInitial

deleted theorem CategoryTheory.Limits.isIso_ι_of_isInitial

deleted theorem CategoryTheory.Limits.isIso_ι_of_isTerminal

modified theorem CategoryTheory.Limits.terminal.hom_ext

deleted def CategoryTheory.Limits.terminalIsoIsTerminal