Commit 2024-10-20 16:57 8d27fbf3
View on Github →feat(CategoryTheory): pull colimits out of hom functors with Yoneda on the LHS (#17440) A technical result on the way towards showing that Ind-objects are closed under filtered colimits.
feat(CategoryTheory): pull colimits out of hom functors with Yoneda on the LHS (#17440) A technical result on the way towards showing that Ind-objects are closed under filtered colimits.