Homotopy Type Theory UMyn8W7b (Rev #37)

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 intervals

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

The elements $[a, b]:\mathcal{I}(\mathbb{Q})$ of the type are the endpoints of the closed rational intervals, which we shall call rational intervals for short.

There is an embedding $i:\mathbb{Q} \to \mathcal{I}(\mathbb{Q})$ defined by

Equality of rational intervals is defined as

Relation to the zero interval

A positive rational interval is defined by

A negative rational interval is defined by

A indefinite rational interval is defined by

Ordering of the intervals

The strict order of the rational intervals is defined as

The opposite strict order of the rational intervals is defined as

The containment relation of the rational intervals is defined as

The opposite containment relation of the rational intervals is defined as

Equality of rational intervals is defined as

Arithmetic of intervals

Zero is defined by

Constants are defined by

Addition is defined by

Negation is defined by

Subtraction is defined by

Scalar multiplication is defined by

One is defined by

Multiplication is defined by

The reciprocal is only defined for intervals that are positive or negative: $0 \lt [a, b]$ or $0 \gt [a, b]$, and is defined by

Division is only defined for intervals in the denominator that are positive or negative: $0 \lt [c, d]$ or $0 \gt [c, d]$, and is defined by

As a result, the rational intervals are a strict quasiordered field.