mathlib3

6161a1fb - feat(category_theory/types): add explicit pullbacks in `Type u` (#6973)

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