Commit 2020-09-13 03:55 f403a8be

View on Github →

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.

Estimated changes

Modified src/category_theory/limits/types.lean

added def category_theory.limits.types.is_limit_equiv_sections

added theorem category_theory.limits.types.is_limit_equiv_sections_apply

added theorem category_theory.limits.types.is_limit_equiv_sections_symm_apply