Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-07 06:34 6161a1fb

View on Github →

feat(category_theory/types): add explicit pullbacks in Type u (#6973) Add an explicit construction of binary pullbacks in the category of types. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/pullbacks.20in.20Type.20u

Estimated changes

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

modified def category_theory.limits.pullback_cone.is_limit_aux

modified def category_theory.limits.walking_cospan.hom.id

modified def category_theory.limits.walking_cospan.hom.inl

modified def category_theory.limits.walking_cospan.hom.inr

modified def category_theory.limits.walking_cospan.left

modified def category_theory.limits.walking_cospan.one

modified def category_theory.limits.walking_cospan.right

modified def category_theory.limits.walking_span.hom.fst

modified def category_theory.limits.walking_span.hom.id

modified def category_theory.limits.walking_span.hom.snd

modified def category_theory.limits.walking_span.left

modified def category_theory.limits.walking_span.right

modified def category_theory.limits.walking_span.zero

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

added def category_theory.limits.types.pullback_cone

added theorem category_theory.limits.types.pullback_iso_pullback_hom_fst

added theorem category_theory.limits.types.pullback_iso_pullback_hom_snd

added theorem category_theory.limits.types.pullback_iso_pullback_inv_fst

added theorem category_theory.limits.types.pullback_iso_pullback_inv_snd

added def category_theory.limits.types.pullback_limit_cone

added def category_theory.limits.types.pullback_obj