home | mathematics | toolbox ::... 1 | 2

Toolbox and the minimalist attitude

From the introduction of Toolbox (by G. Sambin)
Our experience in developing pieces of actual mathematics within type theory has brought us to believe that orthodox type theory is not suitable because its control of information is too strict for this purpose. In fact, the fully analytic character of type theory becomes a burden when dealing with the synthetic methods of mathematics, which `forget' or give for granted most of the details.

This, in our opinion, could be the reason why type theory has collected, up to now, more interest among logicians and computer scientists as a formal system than among mathematicians as a foundational theory. We claim that there is no intrinsic reason why it should remain so, and that actually it is only a matter of developing a stock of `utilities', that is, of building up a toolbox which covers the territory between the basic formalism and mathematical practice.

From the introduction of Minimalist foundation
The purpose of implementing mathematics requires to keep a clear-cut distinction between a ground level with an intensional type theory, which is necessary for implementation and actually is essentially an abstract functional programming language, and a more abstract level, in which one has only extensional concepts and constructs which are needed to develop mathematics.
These extensional tools can be put on top of type theory in the spirit of toolbox [...].

Thus any tool should be obtained according to the forget-restore principle: to reach extensionality, it is necessary to forget some information, like the algorithm to compute a function or the specific proof of a proposition; but to obtain implementation, one has to be able to restore such information at will.
So the formal system must include independent treatment of two different levels of abstraction, as well as a systematic way to connect them. Typically, the axiom of choice is valid at the lower level, while it fails at the extensional level.