Positive open of a locale ($\mathrm{Pos}(a)$)

An open is positive when its positivity truth value holds. Positivity gives a constructive witness of inhabitedness and must not be replaced by double-negated nonemptiness.