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

Commit

5 years ago

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`.

References

#4925 - Make prime-avoidance branch build

Author

b-mehta

Parents

dd43823c

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

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