mathlib

3a99001a - feat(category_theory): Type u is well-powered (#6812)

feat(category_theory): Type u is well-powered (#6812) A minor test of the `well_powered` API: we can verify that `Type u` is well-powered, and show `subobject α ≃o set α`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>