Homotopy Type Theory UMyn8W7b (Rev #42, changes)

Showing changes from revision #41 to #42: 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 semirings

Given a additively cancellative commutative semiring $R$, a 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 semiring is a additively cancellative commutative semiring $R$ for which there exists a function $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)$.

Concrete ETCS

In categorical set theories? such as ETCS?, the set theory is usually a theory of sets and functions? in an abstract category, with elements? being defined as the global elements?, the morphisms? out of the terminal object?. However, this approach poses a few issues, namely that in ordinary mathematical practice, elements are not the same as functions out of the terminal object, although they are isomorphic to each other, and function evaluation of elements in categorical set theories are an abuse of notation.

There are other structural set theories?, such as SEAR, which explicitly put in the elements of a set as a primitive of the theory: this is equivalent to saying that the category is an concrete category rather than an abstract category. In such a presentation involving sets and functions, function evaluation? would be an external version of an evaluation map? defined on the concrete category, making the category into an evaluational category, and the axiom of function extensionality is defined directly on the elements, rather than the global element functions out of the terminal object. The presentation of such a concrete categorical set theory reads more like a traditional presentation of set theory in terms of sets and elements, rather than category theory.

In this presentation, we will be adapting Tom Leinster’s presentation of ETCS to the concrete setting. Some of these axioms might be redundant, but that was true of Tom Leinster’s original presentation.

Primitives

Our theory has the following primitives:

• Some things called sets;

• For every set $A$, these things called elements in $A$, with elements $a$ in $A$ written as $a \in A$;

• For every set $A$ and $B$, these things called functions from $A$ to $B$, with functions $f$ from $A$ to $B$ written as $f:A \to B$;

• For every set $A$ and $B$, an operation called function evaluation assigning every element $a \in A$ and function $f:A \to B$ an element $f(a) \in B$;

• For every set $A$, a function $id_A:A \to A$ called the identity function of $A$;

• For every set $A$, $B$, and $C$, an operation called function composition assigning every function $f:A \to B$ and $g:B \to C$ a function $g \circ f:A \to C$;

Associativity and identity laws

• For every set $A$ and for every element $a \in A$, $id_A(a) = a$.

• For every set $A$, $B$, and $C$, and for every element $a \in A$, $(g \circ f)(a) = g(f(a))$.

…

References

• Tom Leinster?, Rethinking set theory, (arxiv:1212.6543)