From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Thu, 31 May 2018 03:48:01 -0700 (PDT) From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?= To: Homotopy Type Theory Message-Id: <433eba9a-1d5b-43ce-a266-64d2f6b10047@googlegroups.com> In-Reply-To: References: <1527602447.1037774.1389070656.2CE32C72@webmail.messagingengine.com> Subject: Re: [HoTT] Re: Where is the problem with initiality? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1989_993235660.1527763681888" ------=_Part_1989_993235660.1527763681888 Content-Type: multipart/alternative; boundary="----=_Part_1990_379858014.1527763681889" ------=_Part_1990_379858014.1527763681889 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit On Wednesday, 30 May 2018 23:35:57 UTC+1, Michael Shulman wrote: > > > On Tue, May 29, 2018 at 7:00 AM, Jon Sterling > 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 ------=_Part_1990_379858014.1527763681889 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable


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". =C2=A0But 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? =C2=A0The lack of such a definition is not a rea= son
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 theo= ry of groups helped to formulate the notion of a group. The same happened w= ith topology, where formulations of notions of space came after a lot of wo= rk 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
------=_Part_1990_379858014.1527763681889-- ------=_Part_1989_993235660.1527763681888--