Toby Bartels Toby Bartels

This is the personal area of Toby Bartels within the nLab.

Introduction

Here I plan to talk about doing mathematics while taking seriously Errett Bishop's idea of presets. This amounts to founding mathematics on predicative Coquand-style type theory without identity types.

My basic thesis is that allowing identity types makes type theory unnecessarily strong; in particular, it justifies the presentation axiom (and its consequences, such as dependent and countable choice). While identity types seem to be necessary in Martin-Löf-style type theory, in Coquand-style type theory they are not, and so we should make only identity judgements (in fact, only $\beta$-reducibility judgements).

However, the system is still a little stronger than I would like. In particular, adding impredicativity (in the form of a poset of truth values) allows one to construct identity types again. In other words, we still have TV → COSHEP, which does not hold in (for example) Fred Richman's mathematics.

One alternative is simply to look at the desired properties of the category of sets and adopt those as axioms, a constructive ETCS. (For example: the category of sets is a $\Pi$-$W$-pretopos.) But this ruins one of the neat advantages of using presets: a category (internal to the theory now) naturally does not come equipped with a notion of equality of objects, and functors behave like anafunctors by default. (ETA: The main reason that I have not bothered to put anything here is that I believe that HoTT has solved this problem; this axiomatizes the $(\infty,1)$-category of $\infty$-groupoids, inside of which everything is appropriately weak.)

Sometimes I wonder whether mathematics even needs function types; Brouwer's followers still do not accept these in general. (Paul Taylor's ASD is an interesting approach that lacks them, although it is based on extensional equality propositions.) But that is farther than I want to go here.

I welcome comments and corrections, especially from people like Mike and Mathieu who I know have thought about this stuff. (Please place your remarks inside query boxes unless fixing obvious typos.) One specific problem that I ought to solve is to describe the category of contexts of my theory.

Contents

• See preset for an introduction to the basic concept and motivation for the theory.
• etc …