HasBinaryProduct vs HasFiniteProducts

Stream: maths

[Yury G. Kudryashov]

Disclaimer: I'm very far from being a category theory expert.

We have docs#CategoryTheory.Limits.HasBinaryProduct and docs#CategoryTheory.Limits.HasFiniteProducts. What do you think about replacing the latter with [∀ X Y : C, HasBinaryProduct X Y] and proving by induction the current definition?

[Kyle Miller]

That's very different, since it doesn't give you an empty product.

[Yury G. Kudryashov]

Thank you for the explanation. Then should there be a constructor from a universal object and HasBinaryProduct?

[Yury G. Kudryashov]

(or better a lemma saying iff?)

[Kyle Miller]

Yeah, once I'm not on my phone I was going to check if that iff was missing since I noticed it wasn't in that module, before mentioning that we should have it

[Adam Topaz]

docs#CategoryTheory.hasFiniteProducts_of_has_binary_and_terminal

[Adam Topaz]

just in case that's what you wanted Yuri.

[Adam Topaz]

The converse is there as well in terms of instances IIRC, but I don't think we have an iff statement.

[Scott Morrison]

This stuff could definitely use a refactor and cleanup, it is rather old code. But I think keeping the two typeclasses is correct.