Commit 2022-07-03 11:47 024a4231

refactor(category_theory): generalise universe levels in preservation statements (#15067) This big refactoring of universe levels in the category theory library allows to express limit preservation statements like exactness of functors which are between categories that are not necessarily in the same universe level. For this change to make sense for fixed diagrams (like coequalizers or binary products), the corresponding index categories, the universe of which so far was pinned to the category they were used for, is now fixed to Type.