On Wednesday, 30 May 2018 23:35:57 UTC+1, Michael Shulman wrote:
>
>
> On Tue, May 29, 2018 at 7:00 AM, Jon Sterling <j....@jonmsterling.com 
> <javascript:>> wrote: 
> > Far from being a result which might hold or fail about "type theories" 
> (what are those, specifically?), 
>
> I take it that your parenthetical refers to the lack of a general 
> definition of "type theory".  But to me, such a lack is itself a gap 
> in the literature -- how can we really consider "type theory" a 
> respectable mathematical subject if we don't even have definitions of 
> the things it studies?  The lack of such a definition is not a reason 
> not to study type theories in general, rather the opposite -- studying 
> type theories in general will help move us towards being able to 
> formulate such definitions (note the plural -- I don't necessarily 
> expect there to ever be *one* definition encompassing *all* type 
> theories). 
>
>
Of course, as you know, people did a lot of group theory before there was a 
definition of group. And the theory of groups helped to formulate the 
notion of a group. The same happened with topology, where formulations of 
notions of space came after a lot of work on topology had already been 
done. Is the study of type theories mature enough to admit a general 
definition of a type theory, of which the ones we are looking at are a 
particular case?

Martin