Natural numbers from integers

DOI10.1145/3661814.3662129MaRDI QIDQ6970204zbMATH OpenFDO

Authors Christian Sattler, David Wärn

Publication date 18 June 2025

Full work available at URL https://doi.org/10.1145/3661814.3662129

zbMATH Keywords

descenthomotopy type theoryinductive typesintegersnatural numbers

Mathematics Subject Classification ID

Type theory (03B38)

Cites work

• A Brief Overview of Agda – A Functional Language with Dependent Types
• Every elementary higher topos has a natural number object
• Homotopy type theory. Univalent foundations of mathematics
• Internal languages of finitely complete ( , 1)-categories
• Path spaces of higher inductive types in homotopy type theory
• The homotopy theory of type theories
• Two-level type theory and applications

This page was built for publication: Natural numbers from integers

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6970204)