I was going to comment this, but you got here before me. So, I would just like to ramble about type theory and constructive logic a bit. According to the Curry

I was going to comment this, but you got here before me. So, I would just like to ramble about type theory and constructive logic a bit. According to the Curry-Howard correspondence and the BHK interpretation of logic, there is a syntactic correspondence between types and logical formulas and between terms and proofs. Here, the unit type corresponds with truth because it is trivially inhabited with a single inhabitant. The product type A * B is interpreted as logical conjunction because you need a proof of A and a proof of B to inhabit it. The unit type (true) is the identity of the product type (and). Unit * A = A * Unit = A from an isomorphism perspective. From the category theory point of view, a Cartesian monoidal category is a monoidal category where the tensor product is the categorical product and the unit object is the terminal object. It's no coincidence that the terminal object is written as 1. So, an n-ary sequence of propositions connected by ANDs is like an n-ary tuple type, and an empty sequence of propositions connected by ANDs is like the nullary tuple type, or in other words the trivially inhabited unit type.