Settings
I have been studying sequent calculus for several months and found that there should be a rule that is seemingly typical, even too trivial, but/hence no one officially mentions:
$$ \dfrac{ a : A, b : B }{ a, b : A, B }. \tag{1} $$
This seems mere syntax sugar and actually often used in this conventional form:
$$ \vec{x} : \vec{X} \tag{2} $$
as representing:
$$ x_1 : X_1, \dots, x_n : X_n \tag{3} $$
where there seems to be more appropriate one:
$$ \vec{x : X}. \tag{4} $$
By the way, this writing convention $(1)$ performs obviously poor as syntax sugar for heterogeneous A, B, ..., Z since when it becomes longer, you would need to carefully match each element with its own type on each different side of a statement:
$$ a, b, \dots, z : A, B, \dots, Z. \tag{5} $$
Question
My curious question, or intuition, for the whole system of sequent calculus, is:
- Whether we can consider or utilise the rule $(1)$ already as the tensor product introduction, instead of letting it be mere syntax sugar.
- Whether we can introduce sum types $+$, product types $×$, function types $→$ and any other possible ones as parallel to those operations on vectors such as addition, inner product, outer product, element-wise product, Kronecker product, norm, trace, etc.., without loss of generality.
Notes
The proper interpretation of $a, b : A, B$ might be different depending on which side of $⊢$ it is in, the former being tensor product and the latter something like direct sum.
The semantics here is most likely given by polycategory.