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

[Gabriel Scherer <gabriel...@gmail.com>]

Conversely, I think that we could leave the discussion of preterms,
typed/untyped representations, etc., out of the present discussion.
Instead of trying to argue, a priori, which representations gives the
more important initiality statement, we should be able to see, given
initiality proofs for each representation (assuming that the proofs
are as clean as they can), which ones contain the important, tasty
bits, and which ones can be factorized from the others by adding a
trivial or heavy-but-already-well-understood (parsing, for example)
step.
In particular, someone feeling that a given representation is "less
important" from an initiality perspective should be able to prove
themselves correct by deriving the result, while if they are missing
something of mathematical interest it would be apparent in the
difficulty to establish the result.

(It is not clear that the absolute importance of various
representation choices can be assessed solely from their initiality
properties; but initiality properties is what is discussed here.)




On Tue, Jun 5, 2018 at 10:37 AM, David Roberts <drobert...@gmail.com> wrote:
> 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.
>
> --
> 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.