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

[David Roberts <drobert...@gmail.com>]

There is an... "interesting" discussion going on at the fom mailing
list at present, the usual suspects included, about set theory-based
proof assistants, which might provide either a source of entertainment
or frustration. It is enlightening when considering what people think
about typed vs untyped.

Univalent foundations gets a mention here:
https://cs.nyu.edu/pipermail/fom/2018-May/021012.html
The 'ideal proof assistant' is described as being based on ZFC here:
https://cs.nyu.edu/pipermail/fom/2018-May/021026.html
Friedman proclaims he is completely ignorant of the issues and that he
has never gotten close to getting dirty with details, but is happy to
weigh in: https://cs.nyu.edu/pipermail/fom/2018-May/021023.html
The discussion continues this month here:
https://cs.nyu.edu/pipermail/fom/2018-June/021030.html

David
David Roberts
http://ncatlab.org/nlab/show/David+Roberts


On 5 June 2018 at 17:22, Andrej Bauer <andrej...@andrej.com> wrote:
> 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
>
> --
> You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.