The category of types is a monoidal category #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
F is a monoidal functor out of
Type, it takes the (n+1)st cartesian power
of a type to the image of that type, tensored with the image of the nth cartesian power.