Homotopy Type Theory Sandbox (Rev #43, changes)

Showing changes from revision #42 to #43: 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 RR, a term e:Re:R is left cancellative if for all a:Ra:R and b:Rb:R, ea=ebe \cdot a = e \cdot b implies a=ba = b.

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

A term e:Re:R is right cancellative if for all a:Ra:R and b:Rb:R, ae=bea \cdot e = b \cdot e implies a=ba = b.

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

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

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

The multiplicative submonoid of cancellative elements in RR is the subset of all cancellative elements in RR

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

A Euclidean semiring is a additively cancellative commutative semiring RR for which there exists a function d:Can(R)d \colon \mathrm{Can}(R) \to \mathbb{N} from the multiplicative submonoid of cancellative elements in RR to the natural numbers, often called a degree function, a function ()÷():R×Can(R)R(-)\div(-):R \times \mathrm{Can}(R) \to R called the division function, and a function ()%():R×Can(R)R(-)\ \%\ (-):R \times \mathrm{Can}(R) \to R called the remainder function, such that for all aRa \in R and bCan(R)b \in \mathrm{Can}(R), a=(a÷b)b+(a%b)a = (a \div b) \cdot b + (a\ \%\ b) and either a%b=0a\ \%\ b = 0 or d(a%b)<d(g)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 AA, these things called elements in AA, with elements aa in AA written as aAa \in A;

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

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

  • For every set AA, a function id A:AAid_A:A \to A called the identity function of AA;

  • For every set AA, BB, and CC, an operation called function composition assigning every function f:ABf:A \to B and g:BCg:B \to C a function gf:ACg \circ f:A \to C;

Associativity and identity laws

such that

  • For every set AA and for every element aAa \in A, id A(a)=aid_A(a) = a.

  • For every set AA, BB, and CC, and for every element aAa \in A, (gf)(a)=g(f(a))(g \circ f)(a) = g(f(a)).

  • For every set AA and BB and for every function f:ABf:A \to B and g:ABg:A \to B, if f(x)=g(x)f(x) = g(x) for all elements x:Ax \colon A, then f=gf = g.

References

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