All of Vladimir Mikulik's Comments + Replies

I’m confused about Q9.

Given the way $Syn(A,B)$ is defined, it’s unclear to me how we ensure type correctness of $Syn(S_1\times S_1,S_0)$. In what sense is $S_1\times S_1$ a set of sentences (rather than a set of pairs of sentences)? What does an element of that set look like?