Martín Escardó: Mathematical degrees of existence in type theory

Constructive mathematics is often equated with computation. But perhaps a better view (compatible with computation) is that constructive mathematics is about information: information we give, and information is offered to us. In classical mathematics what matters about a theorem is its truth, whereas in constructive mathematics what matters is how much information its formulation and
proof give.

A particular case of existence is disjunction.  For example, in classical mathematics, Goldbach's Conjecture holds or it doesn't (by the excluded-middle postulate). But (both classical and constructive) mathematicians still want to know which one is the case. An answer to the second question gives more information.  In constructive systems such as type theory, it is possible to express mathematically the difference between the information content of the first and second situations.

In this talk I want analyse, mathematically (rather than meta-mathematically or philosophically), the notion of existence in terms of information content. I will show, with definitions, theorems, proofs and examples, that there are many (constructive) degrees of existence, distinguished by the amount of information they give/get.

I will perform this mathematical analysis in Martin-Loef type theory and some univalent extensions. In particular, I will discuss Brouwer's continuity axioms, some of which become false, when rendered in MLTT, if too much existential information is required.