Guardado en:
| Autores principales: | , |
|---|---|
| Formato: | Preprint |
| Publicado: |
2024
|
| Materias: | |
| Acceso en línea: | https://arxiv.org/abs/2405.18388 |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866909212355854336 |
|---|---|
| author | Sattler, Christian Wärn, David |
| author_facet | Sattler, Christian Wärn, David |
| contents | 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 $Σ$, $\mathsf{Id}$, $Π$, and finite colimits with descent (and no universes) admits a natural number type. This improves and simplifies a result by Rose. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2405_18388 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Natural numbers from integers Sattler, Christian Wärn, David Logic in Computer Science Category Theory 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 $Σ$, $\mathsf{Id}$, $Π$, and finite colimits with descent (and no universes) admits a natural number type. This improves and simplifies a result by Rose. |
| title | Natural numbers from integers |
| topic | Logic in Computer Science Category Theory |
| url | https://arxiv.org/abs/2405.18388 |