In Wikipedia article on "Sum Type" it is stated that sum type Curry-Howard correspondence is intuitionistic logical disjoint.
But sum type definition states that it is
a data structure used to hold a value that could take on several different, but fixed, types. Only one of the types can be in use at any one time, and a tag field explicitly indicates which one is in use.
whereas in disjunction you can have both values present at the same time.
To me it looks like sum type is more like a multiplexer than a simple "or", that is $(A\land S) \lor(A \land \lnot S)$, specially because its eliminator acts like a case statement.
I would appreciate if someone can make it clear for me.