Implication Details
Assumptions: natural numbers object, strict terminal object
Conclusions: one-way
Reason: By assumption, is an isomorphism. Therefore, the terminal object is a NNO with and . This precisely means that for all and there is a unique with and . In other words, we have , and therefore (take ), which proves the claim. (From here one can further deduce that the category is thin.)