From Lawvere's paper about ETCS we know that we can do induction for natural number object. My aim is to prove the strong induction principle for an NNO in a topos by translating this argument https://math.ou.edu/~nbrady/teaching/f14-2513/LeastPrinciple.pdf ((I) $\to$ (SI)) into an abstract version, so it works in any category satisfies ETCS. In particular, the axioms of ETCS make sure that we have a Boolean topos.
I think the statement of strong induction to prove in ETCS is as the following.
For a subobject $p: P \to N$, if for an arbitary element $n: 1 \to N$ of the NNO, "all member $n_0: 1\to N$ such that $- \circ \langle n_0, n\rangle = o$ factorises through $P$" implies "$s \circ n: 1 \to N \to N$ factors through P", then $P\cong N$ where $p$ is an isomorphism.
Here $N$ is the NNO, $s: N \to N$ is the successor map the $\le$ relation on NNO is given as the pullback of $o: 1\to N$, as the element $0$ of natural number, along the map truncated subtraction $-: N\times N \to N$, as in Sketch of an elephant by Johnstone (page 114, A2.5).
I am not sure what to do with the $Q$ though, and I am not sure if constructing such a $Q$ need the comprehension axiom for ETCS (which is not in Lawvere's original paper). Hence I have trouble translating the proof in the link to also work for NNO. I think if we translate the proof, then we should reduce the task of $P\cong N$ into the task of proving $Q \cong N$. I am now asking about how to construct such a $Q$, which corresponds to the predicate $Q$ in the link. Any help, please?
If anything I said is wrong, or if there is a better approach, thanks a lot for pointing out!