[Agda] Concepts within Type Theory – Re: [Coq-Club] Type Theory vs. Set Theory – Re: Why dependent type theory?

[Martin Escardo]

On 13/03/2020 16:06, mail at kenkubota.de wrote:
> Concerning constructivism (intuitionism) and intensionality, these are
> philosophical debates with little relevance for mathematics nowadays.

Constructive mathematics may be of little relevance for mathematics - 
and it is for mathematicians to decide for themselves, for their own 
consumption, whether this is really the case.

But clearly constructive mathematics is relevant for computation. I 
understand that most mathematicians are not interested in computation, 
and this is fine (and in fact most computer scientists are not 
interested in constructive mathematics either).

But we now have computers and we compute with them and we want to 
compute more, and constructive mathematics gives a tool to do that - 
among other tools, most of which are based on non-constructive 
mathematics, indeed.

But regarding applications of constructive mathematics to computation, 
for example, a former PhD student of mine, Chuangjie Xu, constructed a 
sheaf topos (in dependent type theory, in its Agda incarnation), for the 
sole purpose of computing a number.

Good luck using a Turing Machine or a Java program for defining and 
computing this number (which Agda computed under a minute).

This number is the modulus of uniform continuity of an arbitrary 
function defined on the Cantor space in a certain kind of laguage 
(spoiler: this language can be chosen to be dependent type theory 
itself, among others).

This may not be progress in mathematics, but it is certainly progress in 
computation / computability (and in logic, if mathematicians are 
suspicious of it as well): We can compute an integer, in theory and in 
practice (and fast), using a Grothendieck topos. Rather than coming up 
with a contrived Turing Machine, or an awkward Java program, or even an 
"elegant" Haskell program, just write a constructive proof - that is, a 
mathematical proof that is like a normal proof but doesn't use excluded 
middle.

I think the mathematics and computer science communities should, at this 
point of history, be joining forces rather than arguing about the sex of 
the angels.

There is only one mathematics, and it includes both non-constructive and 
constructive mathematics. You don't need to like both branches, in the 
same way that you don't need to like every branch of mathematics (and I 
am sure you don't). If you don't like one of them - and I have in mind 
Thorsten and Kevin, please keep quiet and do your own thing, instead of 
insisting that what you do is the ultimately good and correct and 
mainstream and accepted and blessed kind of mathematics. :-)

Best,
Martin