feat(category_theory/limits/shapes): another prototype for special shapes

[semorrison]

This is another attempt at defining a is_binary_products structure, and the conversions back and forth to the general setup.

As an example of use, it allows setting up binary products in Type as:

example : has_binary_products.{v} (Type v) :=
mk' (λ X Y, X × Y) (λ X Y,
  { hom_iso := (λ Q,
    { hom := λ f, (λ q, (f q).1, λ q, (f q).2),
      inv := λ p q, (p.1 q, p.2 q) }) })

@rwbarton, could you have a look at some point?

I'm planning on redoing the existing construction in category_theory/limits/shapes/binary_products.lean of associators and unitors for binary products in this formalism, to test how it works.

If this looks okay, we'll have to do some copy-and-paste for the all the other special shapes.

[jcommelin]

Some typo-fix suggestions and a question.

[jcommelin]

This is certainly the more readable statement. But I wonder if taking the more inherently functorial approach would buy us something down the road. I.e. declare this to be an iso between yoneda.obj P and the product of the yoneda functors of X and Y in the functor category. Of course the naturality part of that iso wouldn't break down so nicely into two parts, but maybe simp-lemma can take care of that.

[jcommelin]

dda5c0c is introducing unique_up_to_canonical_iso, which @kbuzzard will surely like 😉
I do wonder if that should maybe come in its own PR, because now this PR is trying to do 2 things at once.