Commit 2026-04-14 15:27 438f1347

refactor(CategoryTheory): one-field structure morphisms in the category of types (#36613) This PR refactors the category structure on types as follows: We define the one-field structure TypeCat.Fun to wrap a function between types, and a FunLike instance on it. Then we define a one-field structure TypeCat.Hom which wraps a Fun. The morphisms in the category Type u are defined to be TypeCat.Hom, and the FC parameter of the ConcreteCategory instance is TypeCat.Fun. This double nesting allows us to avoid defining a FunLike instance on bare functions, which would give two non-reducibly-defeq coercions from morphisms in Type u to functions. To promote a function to a morphism in this category, we provide the abbreviation TypeCat.ofHom f, as well as a corresponding notation ↾ f. (Entered as \upr.) In the process, we deprecate some declarations that were written specifically for the category of types, such as FunctorToType.map_comp_apply and others, which can now be generated by elementwise. We add a new file Mathlib/CategoryTheory/ConcreteCategory/Representable.lean, which provides some API for the situation when a functor postcomposed by a forgetful functor is representable (the general RepresentableBy API was already unpleasant to work with in this situation, and this PR made this worse, which is the reason for adding the file). We add a new file Mathlib/CartegoryTheory/Limits/ConcreteCategory/Filtered.lean, which provides analogues to some of the API in the CategoryTheory.Limits.Types.FilteredColimit namespace, for concrete categories for which the forgetful functor preserves filtered colimits.