Commit 2024-07-16 09:32 20707571

feat(CategoryTheory): Cat-valued functors induced by passing to Over/Under categories (#14656) This PR redefines but does not rename the natural isomorphisms mapId and mapComp for the composition functors associated to over or under categories. Originally these were defined using isoRefl. Now instead these are defined using eqToIso applied to equalities between the appropriate functors, which are also added here. These equalities are also used to define functors T ⥤ Cat and Tᵒᵖ ⥤ Cat sending an object X to Over X and Under X respectively.