Natural numbers from integers
Christian Sattler, David W\"arn

TL;DR
This paper constructs a natural number type within homotopy type theory from an integer type using basic type-theoretic tools, simplifying previous results and eliminating the need for universes.
Contribution
It introduces a method to derive natural numbers from integers in homotopy type theory using only fundamental type constructions, simplifying prior approaches.
Findings
Natural number type can be derived from integer type in homotopy type theory.
The construction uses only dependent sums, identity types, and extensional dependent products.
The result simplifies and improves previous work by Rose.
Abstract
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 , , , and finite colimits with descent (and no universes) admits a natural number type. This improves and simplifies a result by Rose.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsComputability, Logic, AI Algorithms · Benford’s Law and Fraud Detection · Mathematical and Theoretical Analysis
