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> 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