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

[Martin Escardo <escardo...@googlemail.com>]

On 31/05/18 20:02, Alexander Kurz wrote:

> I am interested in this question of translating the untyped stuff we write on the page into type theory.
> 
> To give a concrete example of what I am thinking of as untyped, but nevertheless conceptual and structural mathematics, I would point at Tom Leinster’s elegant description of the solution to the problem of Buffon’s needle, see the first paragraphs of the section “What is category theory?” at https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html
> 
> I call this argument type free because I see no obvious or canonical way to make the types precise enough in order to implement the proof in, say, Agda. Even if this can be done, it is still important that mathematicians can discuss this argument first without having to make the types precise. So there will always be mathematics outside of type theory.

I don't understand why you call this argument untyped. Do you feel that 
a formalization in set theory, which is untyped, would be easier than a 
formalization in type theory? How is untypedness helping with this argument?

Martin