The definition of Confidential(X) is Point × X, so Confidential(1) should be Point × 1. In reality, our code base treats Confidential(1) as just Point without the unit 1, which is more practical because we can always throw away units, but this goes against the definition of Confidential(X).
The definition of
Confidential(X)isPoint × X, soConfidential(1)should bePoint × 1. In reality, our code base treatsConfidential(1)as justPointwithout the unit1, which is more practical because we can always throw away units, but this goes against the definition ofConfidential(X).