Toby Bartels preset

A preset is like a set without an equality relation. Conversely, a set is a preset $X$ equipped with an equality relation (technically an equivalence prerelation? on $X$).

In his seminal work The Foundations of Constructive Analysis (1967), Errett Bishop explained what you must do to define a set in three steps:

1. You must state what one must do to construct an element of the set;
2. Given two elements constructed as in (1), you must state what one must do to prove that the elements are equal;
3. You must prove that the relation defined in (2) is reflexive, symmetric, and transitive (which can be phrased in similar ‘what one must do’ terms, but that's kind of wordy).

If you only do (1), then you don't have a set, according to Bishop; you only have a preset.

A given preset may define many different sets, depending on the equality relation. For example, the set $\dot{Q}^+$ of positive rational numbers may be defined using the same preset as the set $\dot{Z}^+ \times \dot{Z}^+$ of ordered pairs of positive integers, but the equality relation is different; two pairs $(a,b)$ and $(c,d)$ of integers are equal iff $a = c$ and $b = d$, while two rational numbers $a/b$ and $c/d$ are equal iff $a d = b c$. (Of course, these definitions require that one already have the set $\dot{Z}^+$ of positive integers and the operation of multiplication on it.)

To define the set of rational numbers, there are other methods; indeed $\dot{Q}^+$ and $\dot{Z}^+ \times \dot{Z}^+$ are both isomorphic to $\dot{Z}^+$ (although in different ways), so all this talk of pairs and equality of pairs may be seen as so much syntactic sugar. To define the set of real numbers, however, one really needs to specify the equality relation to avoid getting the non-isomorphic set of regular Cauchy sequences of rational numbers (or something like that). Of course, material set theorists already know how to get around this by encoding equivalence classes as certain sets, but Bishop's point is to avoid such arbitrary (and potentially philosophically confusing) encoding.

In type-theoretic foundations of mathematics, one often gets a category of types (and operations between them) that is not a pretopos; even though such types are sometimes called ‘sets’, they are therefore clearly not the sets that mathematicians (even constructive mathematicians) think of as forming the category of sets. Many type theorists, recognising this, define a set to be a type equipped with an equivalence relation (and a function between sets to be a type-operation that preserves these equivalence relations); then (at least in all of the foundational type theories that I know of) sets do form a pretopos. Some of these type theorists recognise the affinity with Bishop's definition of set and call types ‘presets’ accordingly. Many of these are even inspired to develop preset theory precisely as foundations for Bishop's mathematics.

And here is where I think that they go wrong. Because every foundational type theory (at least of which I am aware) uses identity proposition?s (or identity types if the propositions-as-types paradigm is being used). That is, if $X$ is a type (preset) and $a$ and $b$ are elements of $X$, then there is a proposition $a \equiv_X b$ whose intended meaning is that $a$ and $b$ are identical as elements of $X$. One can try to justify this in terms of Bishop's definition; if you know how $a$ and $b$ are constructed as elements of $X$, then you should be able to decide if they were constructed in exactly the same way, shouldn't you? But you can clearly argue the other side of that, and I don't think that there can be any doubt that having identity propositions violates the spirit of Bishop's definition that you must define how to compare elements for equality. Calling it ‘identity’ instead of ‘equality’ doesn't really change this, and the ability to define a coarser ‘equality’ relation is no different from the ability to define a coarser ‘equivalence’ relation in ordinary set theory. It is almost more honest to call types ‘sets’ and later correct for the fact that these don't form a pretopos by introducing setoids (a set equipped with an equivalence relation), as some type theorists do.

So here I develop foundations for mathematics based on presets as I understand the true spirit of Bishop. Of course, there is not much point to this if it is merely an attempt to properly interpret the holy scriptures. There are practical consequences, the chief one being that COSHEP? (the axiom of set theory that Aczel called ‘presentation’) is no longer justified, nor are its famous consequences, dependent choice? and countable choice?. As far as I know, this is the only non-finitist foundational type theory in this style that does not justify countable choice, moving closer to a type theory for Fred Richman's choice-free constructive mathematics. However, there is a flaw: the axiom COCEOSHEI? holds; as a consequence, if one accepts an impredicative type of propositions? (as Richman in fact does), then COSHEP still follows. So while I do think that my theory of presets is a good interpretation of Bishop, I don't consider it the final word in foundations by any means.

References

• Errett Bishop (1967), Foundations of Constructive Analysis; the relevant material also appears in the updated Constructive Analysis (1985) by Bishop and Douglas Bridges.
• Our own Mathieu Dupont gives a good introduction for what presets can do for category theory (PDF) in an outtake from his thesis.