Re: [HoTT] Re: Where is the problem with initiality?

[Andrej Bauer <andrej...@andrej.com>]

Dear Alexander,


On Wed, May 30, 2018 at 12:53 PM, Alexander Kurz <axh...@gmail.com> wrote:
>
> It is crucial that informal mathematics is untyped. The untypedness is what makes it flexible enough for practical purposes. Formalising mathematics in a proof assistant is hard work. And to a large extent this is due to the fact that everything has to be typed.
>
> If we ever want to get mathematicians to use proof assistants as casually as they use latex, the problem of untyped vs typed mathematics needs to be solved.

I think you made there a coiple of intellectual jumps. In order for
your statements to have some weight, you need to consider the
following questions:

(a) What if formalization of mathematics in existing proof assistants
is hard for some reason other than typedness?

(b) Most proof assistants that have a large user base are typed. Is
this is a big conspiracy on part of the designers, or could it be
understood as evidence that typed proof assistants have a certain
advantage over the untyped ones?

(c) You offer LaTeX as an example of good design. I beg to differ.

(d) Informal mathematics is very obviously typed, as witnessed by the
fact that authors are always carefully explain the types of various
symbols they use (or rely on the culturally accepted notations).

The Buffon needle example presents absolutely no obstacle to typing.
Perhaps you are mixing up *informal* nature of human mathematics with
untypedness? Formalizing Buffon's needle requires a great amount of
precision (what is a curve? what does it mean to "throw a needle"? how
do we cuunt crossings when there are infinitely many?) which is
unavoidable so long as we subbscribe to the mathematical method.
Typedness has nothing to do with this fact.

With kind regards,

Andrej