Homotopy Type Theory UMyn8W7b (Rev #44, changes)

Showing changes from revision #43 to #44: Added | ~~Removed~~ | ~~Chan~~ged

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$ .

\mathrm{isLeftCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(e \cdot a = e \cdot b) \to (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$ .

\mathrm{isRightCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(a \cdot e = b \cdot e) \to (a = b)

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

\mathrm{isCancellative}(e) \coloneqq \mathrm{isLeftCancellative}(e) \times \mathrm{isRightCancellative}(e)

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

\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)

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$ ;

~~such that~~

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))$ .

For every set $A$ and $B$ and for every function $f:A \to B$ and $g:A \to B$ , if $f(x) = g(x)$ for all elements $x \colon A$ , then $f = g$ .

~~References~~

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

Revision on May 15, 2022 at 03:13:00 by Anonymous?. See the history of this page for a list of all contributions to it.