Homotopy Type Theory UMyn8W7b (Rev #36)

On foundations

The natural numbers are characterized by their induction principle (in second-order logic/in a higher universe/as an inductive type). If one only has a first order theory, then one cannot have an induction principle, and instead one has a entire category of models. Thus, the first order models of arithmetic typically found in classical logic and model theory do not define the natural numbers, and this is true even of first-order Peano arithmetic.

Closed rational interval arithmetic

The endpoints of closed rational intervals are a subset of the product type $\mathbb{Q} \times \mathbb{Q}$, defined as:

The elements $[a, b]:\mathrm{ClosedIntervalEndpoints}(\mathbb{Q})$ of the type are the endpoints of the closed rational intervals.