On Thursday, 31 May 2018 20:02:51 UTC+1, Alexander Kurz wrote:
>
>
> > On 31 May 2018, at 12:05, Michael Shulman <shu...@sandiego.edu 
> <javascript:>> wrote: 
> > 
> > It sounds like Thorsten and are both starting to repeat ourselves, so 
> > we should probably spare the patience of everyone else on the list 
> > pretty soon.  I'll just make my own hopefully-final point by saying 
> > that if "properties of the typed algebraic syntax" can imply that the 
> > untyped stuff we write on the page has a *unique* typed denotation, 
> > independent of a particular typechecking algorithm, as mentioned in my 
> > last email, then I'll (probably) be satisfied.   
>
> 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