# Zulip Chat Archive

## Stream: maths

### Topic: finite prods from binary prods

#### Kevin Buzzard (Dec 07 2019 at 15:48):

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 (Dec 07 2019 at 15:59):

I think your first sentence is in mathlib

#### Johan Commelin (Dec 07 2019 at 15:59):

@Scott Morrison did that a while ago, I think

#### Kevin Buzzard (Dec 07 2019 at 16:21):

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 (Dec 07 2019 at 23:23):

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

.

Last updated: May 18 2021 at 07:19 UTC