Actually, that `Inductive nat` is precisely a natural number object in terms of categorial semantics - it's worth mentioning that NNO's in categorial semantics

Actually, that `Inductive nat` is precisely a natural number object in terms of categorial semantics - it's worth mentioning that NNO's in categorial semantics are unique up to isomorphism. That "Inductive" syntax in Coq is actually a key part of the system, it's involved in defining things as basic as equality and product- or sum-types. This is quite different from how things would be done in a "standard" set theory.