finite prods from binary prods

Stream: maths

[Kevin Buzzard]

To prove that if a category has a terminal object and binary products then it has all finite products, it would be natural to first prove that if it has binary products and all limits of shapes J1 and J2, then it has all limits of shape J1 disjoint-union J2. Is this in mathlib? I couldn't even find the disjoint union construction, but I'm only just beginning to find my way around the library.

[Johan Commelin]

I think your first sentence is in mathlib

[Johan Commelin]

@Scott Morrison did that a while ago, I think

[Kevin Buzzard]

Calle was trying to learn the category theory library by setting himself basic questions like this. I think it's a pretty neat idea.

[Scott Morrison]

No, this isn't done in mathlib. There's just a stub at src/category_theory/limits/shapes/constructions/finite_products.lean.