Commit 2024-02-14 19:13 30e83bf0
View on Github →feat: finality of a certain functor related to colimits of representable presheaves (#10339) This is the final missing ingredient of the recognition theorem for Ind-objects (Prop. 4.8), so after this is done it's probably finally time to get the definition of an Ind-object into mathlib.