Commit 2024-10-04 10:12 2a16a7b0

refactor(CategoryTheory): generalize universes for representable functors (#17389) Functor.Representable is renamed Functor.IsRepresentable, and the API now allows any universe for the target category of types: in the definition, we use natural bijections instead of natural isomorphisms between functors to types. A new structure Functor.RepresentableBy is introduced: it contains the data expressing that a functor F : Cᵒᵖ ⥤ Type _ is representable by an object Y : C.