From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 1 Jun 2018 14:06:17 -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: <dd79e236-a55d-4f14-b320-41966563bc14@googlegroups.com>
In-Reply-To: <CAA3CDBagp=z5f-h3gBamc-dV7eUSb07s7eZUwf0qau-efNEZXg@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> <1efa5fe9-cdc9-4714-ae2a-953ac59cfdf4@googlegroups.com>
 <CAA3CDBagp=z5f-h3gBamc-dV7eUSb07s7eZUwf0qau-efNEZXg@mail.gmail.com>
Subject: Re: [HoTT] Re: Where is the problem with initiality?
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_10989_771158188.1527887177633"

------=_Part_10989_771158188.1527887177633
Content-Type: multipart/alternative; 
	boundary="----=_Part_10990_1676661294.1527887177633"

------=_Part_10990_1676661294.1527887177633
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable



On Friday, 1 June 2018 21:59:28 UTC+1, Andr=C3=A1s Kov=C3=A1cs wrote:
>
> I like this question. If the syntax is supposed to be the initial model,=
=20
>> then it can't be a set.
>
>
> Why?=20
>

I don't think the initial model is a set. Is it?

Martin
=20

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

<div dir=3D"ltr"><br><br>On Friday, 1 June 2018 21:59:28 UTC+1, Andr=C3=A1s=
 Kov=C3=A1cs  wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;ma=
rgin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=
=3D"ltr"><span style=3D"color:rgb(80,0,80);font-family:arial,sans-serif;fon=
t-size:12.8px;font-style:normal;font-weight:400;letter-spacing:normal;text-=
align:start;text-indent:0px;text-transform:none;white-space:normal;word-spa=
cing:0px;background-color:rgb(255,255,255)"><blockquote class=3D"gmail_quot=
e" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204)=
;padding-left:1ex"><span style=3D"color:rgb(34,34,34);font-family:arial,san=
s-serif;font-size:12.8px;font-style:normal;font-weight:400;letter-spacing:n=
ormal;text-align:start;text-indent:0px;text-transform:none;white-space:norm=
al;word-spacing:0px;background-color:rgb(255,255,255);float:none;display:in=
line">I like this question. If the syntax is supposed to be the initial mod=
el, then it can&#39;t be a set.</span></blockquote><div><br></div></span><d=
iv style=3D"color:rgb(34,34,34);font-family:arial,sans-serif;font-size:12.8=
px;font-style:normal;font-weight:400;letter-spacing:normal;text-align:start=
;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;ba=
ckground-color:rgb(255,255,255)">Why?=C2=A0</div></div></blockquote><div><b=
r></div><div>I don&#39;t think the initial model is a set. Is it?</div><div=
><br></div><div>Martin</div><div>=C2=A0</div></div>
------=_Part_10990_1676661294.1527887177633--

------=_Part_10989_771158188.1527887177633--