> On 31 May 2018, at 12:05, Michael Shulman <shu...@sandiego.edu> 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.