How about with the following one?
data N+ : N -> Set where
pos : forall {n : N} -> N+ (succ n)
Since Agda provides non-exhaustive pattern-matching, I believe, you
don't need to worry about positiveness.
(Cf. Ulf Norell's "Dependently Typed Programming in Agda")