Homotopy Type Theory UMyn8W7b (Rev #40, changes)

Showing changes from revision #39 to #40: Added | Removed | Changed

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.

Euclidean rings

Given a additively cancellative commutative semiringcommutative ring$R$ , a term$e:R$ R e:R , a is term$e:R$ is left cancellative if for all $a:R$ and $b:R$, $e \cdot a = e \cdot b$ implies $a = b$.

A term $e:R$ is right cancellative if for all $a:R$ and $b:R$, $a \cdot e = b \cdot e$ implies $a = b$.

An term $e:R$ is cancellative if it is both left cancellative and right cancellative.

The multiplicative submonoid of cancellative elements in $R$ is the subset of all cancellative elements in $R$

A Euclidean ring semiring is a additively cancellative commutative semiringcommutative ring$R$ for which there exists a function$d:\mathrm{Can}(R)\to \mathbb{N}$ R d \colon \mathrm{Can}(R) \to \mathbb{N} for from which the there multiplicative exists submonoid a of cancellative elements infunction?$R$ to the$d \colon \mathrm{Can}(R) \to \mathbb{N}$ from the multiplicative submonoid of cancellative elements in $R$ to the natural numbers, often called a degree function, a function $(-)\div(-):R \times \mathrm{Can}(R) \to R$ called the division function, and a function $(-)\ \%\ (-):R \times \mathrm{Can}(R) \to R$ called the remainder function, such that for all $a \in R$ and $b \in \mathrm{Can}(R)$, $a = (a \div b) \cdot b + (a\ \%\ b)$ and either $a\ \%\ b = 0$ or $d(a\ \%\ b) \lt d(g)$.