[Merged by Bors] - feat(category_theory/types): add explicit pullbacks in Type u

[gnprice]

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

---

The construction of the is_limit feels messy to me -- that's an area where I'd be especially glad for suggestions on how to write it better, though really I'm happy to hear feedback anywhere.

I don't love these names, partly because I don't feel like they particularly signal the distinction between these explicit pullbacks and the general ones provided by the has_pullbacks instance through category_theory.limits.pullback, category_theory.limits.pullback.fst, and so on. I'm not sure what would be the best names to use instead, though. Perhaps the most reasonable way to express that distinction is just the difference in namespace -- category_theory.limits.foo vs. category_theory.limits.types.foo? In that case perhaps most of these should just go under the pullback sub-namespace: so category_theory.limits.types.pullback.fst and so on.

In the module docstring at the top of the file, it seemed like a couple of existing features were missing from the inventory, so I added those along with this one. I think a couple of other parts of that module docstring need updates for refactors that have happened -- I don't see limit_data or types_has_terminal mentioned in the code -- but I'm not sure what the right story is for each of those, so those updates may be easier to get right for someone more familiar with the history of this file.

[semorrison]

I'll suggest an alternative approach on zulip!

[bryangingechen]

(For future reference: Scott's Zulip thread is here.)

[gnprice]

Thanks @semorrison for the review!

I've pushed a new version which I believe addresses all your comments (here and on Zulip.) See also my reply about @[pattern] above at #6973 (comment) .

[semorrison]

Suggested change

	@[simp] lemma pullback_fst'
	: (pullback_iso_pullback f g).hom ≫ (λ p, (p : X × Y).fst) = pullback.fst :=
	@[simp] lemma pullback_fst' :
	(pullback_iso_pullback f g).hom ≫ (λ p, (p : X × Y).fst) = pullback.fst :=

[semorrison]

I'm not convinced these simp lemmas will ever actually fire -- it seems unlikely the left hand side would ever appear as stated. I wonder if the elementwise version of these lemmas would be more useful.

On the other hand, the lemmas for (pullback_iso_pullback f g).inv should be stated, and seem fine as simp lemmas.

[gnprice]

Sure. I added simp lemmas for (pullback_iso_pullback f g).inv, and replaced these with elementwise versions.

The elementwise versions I came up with feel a bit messy to me -- but take a look and see what you think.

[gnprice]

Thanks! New version pushed.

[semorrison]

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests

[gnprice]

Thanks for all the reviews!