Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-04 09:44 9a8e9fa5

View on Github →

chore(category_theory/limits): Generalize universes for preserves/shapes/pullback.lean (#10780)

Estimated changes

Modified src/category_theory/limits/constructions/epi_mono.lean

Modified src/category_theory/limits/functor_category.lean

deleted def category_theory.limits.preserves_colimits_of_evaluation

modified def category_theory.limits.preserves_colimits_of_shape_of_evaluation

deleted def category_theory.limits.preserves_limits_of_evaluation

modified def category_theory.limits.preserves_limits_of_shape_of_evaluation

added def category_theory.limits.{w'

Modified src/category_theory/limits/is_limit.lean

added def category_theory.limits.is_colimit.of_whisker_equivalence

added def category_theory.limits.is_colimit.whisker_equivalence_equiv

added def category_theory.limits.is_limit.of_whisker_equivalence

added def category_theory.limits.is_limit.whisker_equivalence_equiv

Modified src/category_theory/limits/preserves/limits.lean

Modified src/category_theory/limits/preserves/shapes/pullbacks.lean

modified def category_theory.limits.is_colimit_of_has_pushout_of_preserves_colimit

modified def category_theory.limits.is_limit_of_has_pullback_of_preserves_limit

modified def category_theory.limits.preserves_pullback_symmetry

modified def category_theory.limits.preserves_pushout_symmetry

Modified src/category_theory/limits/shapes/pullbacks.lean

added def category_theory.limits.walking_cospan_equiv

added def category_theory.limits.walking_cospan_functor

added theorem category_theory.limits.walking_cospan_functor_id

added theorem category_theory.limits.walking_cospan_functor_inl

added theorem category_theory.limits.walking_cospan_functor_inr

added theorem category_theory.limits.walking_cospan_functor_left

added theorem category_theory.limits.walking_cospan_functor_one

added theorem category_theory.limits.walking_cospan_functor_right

added def category_theory.limits.walking_span_equiv

added def category_theory.limits.walking_span_functor

added theorem category_theory.limits.walking_span_functor_fst

added theorem category_theory.limits.walking_span_functor_id

added theorem category_theory.limits.walking_span_functor_left

added theorem category_theory.limits.walking_span_functor_right

added theorem category_theory.limits.walking_span_functor_snd

added theorem category_theory.limits.walking_span_functor_zero