In homotopy type theory, a natural number type is freely generated by an element and an endomorphism. Similarly, an integer type is freely generated by an element and an automorphism. Using only dependent sums, identity types, extensional dependent products, and a type of two elements with large elimination, we construct a natural number type from an integer type. As a corollary, homotopy type theory with only $\Sigma$, $\mathsf{Id}$, $\Pi$, and finite colimits with descent (and no universes) admits a natural number type. This improves and simplifies a result by Rose.

翻译：在同伦类型论中，自然数类型由一个元素和一个自同态自由生成。类似地，整数类型由一个元素和一个自同构自由生成。我们仅使用依赖和、恒等类型、外延依赖积以及具有大消去性质的双元素类型，从整数类型构造出自然数类型。作为推论，仅包含$\Sigma$、$\mathsf{Id}$、$\Pi$以及具有下降性质的有限余极限（且不含宇宙）的同伦类型论，允许存在自然数类型。这一结果改进并简化了Rose的结论。