The constructive meaning of a set is that that membership should be decidable, not just semi-decidable.
You can encode semidecidable sets constructively as functions into Σ, where Σ is the Sierpinski type.
The Sierpinski type can be encoded various ways, e.g. coinductively by generators True:Σ and Maybe:Σ→Σ subject to the quotient relation Maybe(x)=x, which leads to two values, True and False:=Maybe(False).
The Sierpinski type is closed under countable disjunctions and finite conjunctions, and therefore functions into it are closed under countable unions and finite intersections. In classical math, excluded middle implies that the Sierpinski type, the booleans, and the truth values are all isomorphic, but in constructive math these equivalences are taboo. In particular, the not function on the Sierpinski type is taboo, and would imply that the Sierpinski type is isomorphic to booleans.
You can encode semidecidable sets constructively as functions into Σ, where Σ is the Sierpinski type.
The Sierpinski type can be encoded various ways, e.g. coinductively by generators True:Σ and Maybe:Σ→Σ subject to the quotient relation Maybe(x)=x, which leads to two values, True and False:=Maybe(False).
The Sierpinski type is closed under countable disjunctions and finite conjunctions, and therefore functions into it are closed under countable unions and finite intersections. In classical math, excluded middle implies that the Sierpinski type, the booleans, and the truth values are all isomorphic, but in constructive math these equivalences are taboo. In particular, the not function on the Sierpinski type is taboo, and would imply that the Sierpinski type is isomorphic to booleans.