{-
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