From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 1 Jun 2018 12:55:06 -0700 (PDT)
From: =?UTF-8?Q?Mart=C3=ADn_H=C3=B6tzel_Escard=C3=B3?=
 <escardo...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Message-Id: <1efa5fe9-cdc9-4714-ae2a-953ac59cfdf4@googlegroups.com>
In-Reply-To: <CAGYJgtaFm3OTCWBbeyZrrpVdqYH7GbFbyTT7O9t0gEhSfW5fpg@mail.gmail.com>
References: <CAOvivQxmrTLRW8wk7cu+A9zF3LCrXSfqsp6R2UN_sz9tF-5UHQ@mail.gmail.com>
 <CAOvivQyY1k+KE9PztsNq6uhZGuV9D3pOYznnbB4p81s4=iHK0g@mail.gmail.com>
 <06B9C5AB-C7CB-4CB5-B951-64E0C4180AD9@exmail.nottingham.ac.uk>
 <CAOvivQw+-fuPg=8gd=cvTsY++iqH4+=B4QRHQcm8vK6FwQSkGg@mail.gmail.com>
 <20180530093331.GA28365@mathematik.tu-darmstadt.de> <5559377C-94C9-422E-BBF7-A07AFA4B7D04@exmail.nottingham.ac.uk>
 <3D1D292E-1EFF-4EA2-8233-B55FDA5CE8A5@gmail.com> <5A8268CE-26C1-4FD5-A82F-8063C08EF115@exmail.nottingham.ac.uk>
 <CAOvivQzSuvhvvhLs0jR2ADTPUR9cKG2NucADJqe=Oer_EB0aaQ@mail.gmail.com>
 <D040F1EA-B812-4703-87CD-840E80DBE5CA@exmail.nottingham.ac.uk>
 <CAOvivQzU1M1gh63RxegZWuzw2LT2b-vsUuSEiB49LAOgJouW6Q@mail.gmail.com>
 <37CBB960-C4F1-4B97-92E6-28462A0591C1@gmail.com> <2b190a31-7985-4e6b-9f69-ed244ea64d7d@googlegroups.com>
 <CAGYJgtaFm3OTCWBbeyZrrpVdqYH7GbFbyTT7O9t0gEhSfW5fpg@mail.gmail.com>
Subject: Re: [HoTT] Re: Where is the problem with initiality?
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_9836_1977809593.1527882906722"

------=_Part_9836_1977809593.1527882906722
Content-Type: multipart/alternative; 
	boundary="----=_Part_9837_691039860.1527882906723"

------=_Part_9837_691039860.1527882906723
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit



On Friday, 1 June 2018 18:45:42 UTC+1, Eric Finster wrote:
>
> I guess my question is pretty simple: why should we insist,
> as Thorsten seems to, that the "intrinsic" syntax of type
> theory form a set?
>

I like this question. If the syntax is supposed to be the initial model, 
then it can't be a set.

 Martin


------=_Part_9837_691039860.1527882906723
Content-Type: text/html; charset=utf-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><br><br>On Friday, 1 June 2018 18:45:42 UTC+1, Eric Finste=
r  wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-left: =
0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr"><div=
 style=3D"font-size:13px">I guess my question is pretty simple: why should =
we insist,</div><div style=3D"font-size:13px">as Thorsten seems to, that th=
e &quot;intrinsic&quot; syntax of type</div><div style=3D"font-size:13px">t=
heory form a set?</div></div></blockquote><div><br></div><div>I like this q=
uestion. If the syntax is supposed to be the initial model, then it can&#39=
;t be a set.</div><div><br></div><div>=C2=A0Martin</div><div><br></div></di=
v>
------=_Part_9837_691039860.1527882906723--

------=_Part_9836_1977809593.1527882906722--