Discrepancy of unique of Product and unique of IsPullback

[sergey-goncharov]

Binary products are special pullbacks. The current implementation of IsPullback in Categories.Diagram.Pullback almost conforms to the corresponding definition of binary products in Categories.Object.Product.Core, except one little twist: in the conclusion of the unique field the universal morphism is on the left in one case and on the right in the other case. Perhaps, this should be unified. It is probably easier to accept the order, as in products.

[JacquesCarette]

I agree that the order in Product is the better one. Especially as one sees uses of converse to prove very simple things using pullback, which is a hint that the order is wrong.