empty and binary imply finary

Stream: condensed mathematics

[Kevin Buzzard]

@Adam Topaz I have been snowed under with teaching recently. I am trying to pick up some pieces. A couple of months ago before it all hit wasn't I working on some category theory statement of the form "if it works for initial objects and binary products then it works for finite products". I'm pretty sure I never finished it. I'm wondering whether I should pick it up as an example in my course

[Adam Topaz]

I finished it off a few weeks ago ;)

[Kevin Buzzard]

Many thanks! IIRC I was struggling (read : learning a lot about how to do category theory in Lean) even with the simple way.

[Adam Topaz]

The argument is not ideal… we have https://leanprover-community.github.io/mathlib_docs/category_theory/limits/constructions/finite_products_of_binary_products.html#category_theory.preserves_finite_products_of_preserves_binary_and_terminal which should have given this to us for “free”, except that the universes don’t quite match. Maybe someone with more energy than I have could generalize the universes there…

[Adam Topaz]

In any case, I did use a variant of docs#fintype.induction_empty_option which worked out quite well!