{- This is the formalization accompanying the paper Natural numbers from integers by Christian Sattler and David Wärn to appear at LiCS 2024 The formalisation follows the first approach of the paper. Lemmas in the paper link to corresponding parts of the formalization where appropriate. Notes * The formalization has been confirmed to type-check with Agda 2.6.4.3. * We consistently avoid universes. We sometimes use the type universe `Set` of Agda, but never mention any larger types or universe levels. All our mentions of Set fall into the following categories: - Constructing a type (for example, `Σ A B : Set` for fixed A and B). - Constructions parametrized by a type or family of types (for example, the parameters A and B in `Σ A B`). - Large elimination over binary coproducts (only in **Booleans.agda**). Therefore, all occurrences of "Set" translate into the universe-free type theory of the paper that explicitly handles types instead. * We work with isomorphisms (in the sense of an inverse map with two homotopies) instead of equivalences throughout. Nowhere in this formalisation do we consider equalities of isomorphisms (which would be a reason to use equivalences instead). Integer induction phrased using isomorphisms is interderivable with integer induction phrased using equivalences (since being an isomorphism is logically equivalent to being an equivalence and sections of integer inductions only involve the forward map of the equivalence/isomorphism). * We try to mark definitions as abstract when possible, both to make it clear to the reader what parts are proof irrelevant, and to help Agda infer implicit arguments. Note that abstract blocks in the same module share their abstraction scope. We do not rely on this behaviour. * In Agda, the equality symbol `=` denotes judgmental equality. In our formalisation, we use `≡` for typal equality. Note that the paper uses the reverse convention. -} -- Overview of modules {- This file develops some preliminaries that you would normally find in a library. It starts out with the type formers used in the formalisation (e.g. id, +, and bottom, which are the only inductive types we declare) and postulates funext. The rest of the file is devoted to some basic reasoning about equality, isomorphisms and the fact that various type formers respect isomorphism. -} import Preliminaries -- This file contains a proof that any map with a two-sided inverse has contractible fibres. import Equivalences {- This file defines the type of fix points of a map and proves the rolling rule. The rolling rule itself is a composition of two isomorphisms each of which is defined directly by pattern matching. This construction computes as expected on the first component of the sigma-type of fix points. -} import RollingRule {- This file defines what an integer algebra is, what a displayed integer algebra is, and what a section of a displayed integer algebra is. We postulate that there is an integer algebra ℤ and that every displayed integer algebra over ℤ has a section. We derive some direct consequences in the same file. -} import IntegerAlgebra -- Analogous to the previous file, but for natural number algebras and without postulates. import NatAlgebra -- Defines subtraction of integers by integer recursion and proves some basic lemmas. import Subtraction -- Constructs the isomorphism ℤ = ℤ + ℤ and derives the map ℤ → ℤ + ℤ + ℤ. import Doubling {- Some trivial facts about coproducts A + B and the two predicates on such a type which tell whether an element is in the left or right part. This is the only part where we use large elimination (descent) for +. -} import Booleans {- This file specialises some definitions from Booleans.agda along the map ℤ → ℤ + ℤ + ℤ. Also defines the strict ordering < on ℤ and proves a couple of basic properties. -} import Signs {- This file defines the type M of nonnegative integers and proves that it is freely generated by a map ℤ⁰ → M and an endomorphism M → M, using the idea of inductive functions and the rolling rule. -} import M {- This file defines the rectification endomorphism M → M and the naturals as the type of fixed points of this map. We establish the final result of the formalisation: the type of naturals thus defined has elimination, i.e. a section of any displayed natural numbers algebra. -} import Naturals