tprod

Stream: general

[Johan Commelin]

there are currently two PRs that introduce tprod:

• #5311 for indexed tensor products
• #5385 for finite products of types

I don't have a strong opinion. But it would be good to resolve the conflict before merging.
cc: @Floris van Doorn @Frédéric Dupuis

[Eric Wieser]

tprod seems like a natural extension of tmul to me, so I'd favor letting 5311 keep the name and renaming the other.

[Floris van Doorn]

Ok, I'll rename it. How about typeprod? (I prefer a name without underscore, because I'm planning to have lemmas with names like typeprod_typeprod.)

[Mario Carneiro]

list.tprod?

[Mario Carneiro]

I would also like to see if we can avoid it entirely

[Floris van Doorn]

I'm happy with list.tprod, then I will also define set.tprod and measure.tprod.
I think this is the most convenient way to do things, see comment in #5385

[Mario Carneiro]

That seems fine to me, as long as the use is limited to these kind of proofs and isn't some new "vocabulary type" that we want to prove all sorts of things about

[Yakov Pechersky]

A question about #5385, defining using foldr places a punit at the end of the product. Why not a foldr1, so that the list of two elements is more directly equivalent to the regular Cartesian product, etc?

[Mario Carneiro]

that makes the inductive arguments more complicated, especially here where defeq is important

[Mario Carneiro]

using foldr1 would mean that pempty is either a special case or not included at all

[Floris van Doorn]

Indeed, I care more about simple proofs than a superfluous × punit, so I prefer foldr.