computability – Is it valid to make an admission of a topological space by a “partial quotient map”?

It is well-known that the Sierpiński space, ${0,1}$ endowed with topology ${emptyset, {0},{0,1}}$, is admissible. I tried to implement it in Haskell.

First I implement $mathbb{N}$ (including zero; some topologists might prefer denoting it by $S_omega$) by Peano definition:

data Peano = Zero | Succ Peano deriving (Eq, Ord)

This encodes $mathbb{N}$, but there is one additional value lurking behind: fix Succ. I denote it by $omega$, and I denote $mathbb{N} cup {omega}$ by $overline{S_omega}$. We observe that $overline{S_omega}$ is in order topology.

I abuse this fact and implement the Sierpiński space by taking a quotient space. The quotient map $q$ is:

q(o) =
0 & text{if } o < omega \
1 & text{o.w.}

In Haskell, This can be realized by:

newtype Sierpinski = Sierpinski Peano

instance Eq Sierpinski where
    Sierpinski m == Sierpinski n = let
        q m = case m of
            Zero   -> False
            Succ n -> q n
        in q m == q n

But to think about it, q doesn’t halt on fix Succ. In other words, q is partial, and doesn’t match $q$. Is this really a valid implementation of the Sierpiński space?