Commit 2025-10-29 00:35 d54a7d03

View on Github →

feat(CategoryTheory/Limits): precomposition with final functors and ColimitType (#30779) We obtain a dual result to #30403 for the interaction between final functors and colimits of functors to types. This is phrased using the universe generic Functor.ColimitType. (We also improve the proof of #30403)

Estimated changes

Modified Mathlib/CategoryTheory/IsConnected.lean

added theorem CategoryTheory.constant_of_preserves_morphisms'

Modified Mathlib/CategoryTheory/Limits/Final/Type.lean

added theorem CategoryTheory.Functor.bijective_colimitTypePrecomp

added def CategoryTheory.Functor.colimitTypePrecomp

added theorem CategoryTheory.Functor.colimitTypePrecomp_ιColimitType

Modified Mathlib/CategoryTheory/Limits/Types/ColimitType.lean

added def CategoryTheory.Functor.CoconeTypes.precomp