Commit 2024-09-09 12:18 a057331e

feat:(CategoryTheory): C ⥤ D is enriched over C ⥤ Type (#13841) This PR shows that C ⥤ D is enriched over C ⥤ Type max v' v u where C : Type u with [Category.{v} C] and [Category.{v'} D]. To do this, a hom-object is constructed for functors F G : C ⥤ D. Applies in particular to simplicial objects being enriched over simplicial sets.