feat(category_theory/limits/types): is_limit versions of limits in type (#4130)
feat(category_theory/limits/types): is_limit versions of limits in type (#4130)

`is_limit` versions for definitions and lemmas about limits in `Type u`.



leanprover-community/mathlib,leanprover-community/mathlib