From mboxrd@z Thu Jan 1 00:00:00 1970 Date: Fri, 24 Feb 2017 06:36:57 -0800 (PST) From: Paolo Capriotti To: Homotopy Type Theory Cc: benedik...@gmail.com, vlad...@ias.edu, univalent-...@googlegroups.com, homotopyt...@googlegroups.com Message-Id: <3a11ec4a-ae2a-47ab-ae04-3f2115cb1d9e@googlegroups.com> In-Reply-To: <4796BE9D-E759-4F57-A3AB-8F8808C01D76@ias.edu> References: <1FFF5B8D-06FC-4ECD-8F89-496A4C2E3A3A@ias.edu> <484524d2-4054-5b7a-14af-e68a8e4b8375@gmail.com> <91160F61-2A67-4B1F-9A4A-F3510B99E9D3@ias.edu> <29b2bdf5-3838-a268-5a44-4aea998cb878@gmail.com> <4796BE9D-E759-4F57-A3AB-8F8808C01D76@ias.edu> Subject: Re: [HoTT] about the HTS MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_234_1314358376.1487947017752" ------=_Part_234_1314358376.1487947017752 Content-Type: multipart/alternative; boundary="----=_Part_235_1699592489.1487947017752" ------=_Part_235_1699592489.1487947017752 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 7bit >> On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens >> wrote: >> >> Section 1.4.8 "Equality" gives an informal account and points >> to several >> precise definitions. >> On page 43 two equality types are considered, one intensional >> one and >> one with reflection rule. I haven't actually considered something like what Vladimir suggested, though. In the systems that I described in my thesis, exact equality is defined for every type. Vladimir Voevodsky writes: > BTW It is a little dangerous to define presheaves as functors C > -> Sets^{op}. While it gives the correct objects, the morphisms > between presheaves are not morphisms in the category of functors > C -> Sets^{op} but in the opposite category. Ah, right. The reason why I defined presheaves this way is that you can just say that the slice category over a presheaf $P$ is presheaves over the category of elements of $P$, rather than copresheaves, so it's more uniform and certain proofs become a little bit nicer. Of course, one could start with C^{op} and use copresheaves throughout, but then I think things would get quite confusing with the Yoneda embedding. But thanks for pointing out this problem. Somehow, it had never occured to me that natural transformations are going in the wrong direction with my definition. Paolo ------=_Part_235_1699592489.1487947017752 Content-Type: text/html; charset=utf-8 Content-Transfer-Encoding: quoted-printable
>> On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens= =C2=A0
>> <benedi...@gmail.com> wrote:
>= >=C2=A0
>> Section 1.4.8 "Equality" gives an i= nformal account and points=C2=A0
>> to several
&g= t;> precise definitions.
>> On page 43 two equality type= s are considered, one intensional=C2=A0
>> one and
>> one with reflection rule.

I haven't= actually considered something like what Vladimir=C2=A0
suggested= , though. =C2=A0In the systems that I described in my thesis,=C2=A0
exact equality is defined for every type.

Vladi= mir Voevodsky writes:
> BTW It is a little dangerous to define= presheaves as functors C=C2=A0
> -> Sets^{op}. While it gi= ves the correct objects, the morphisms=C2=A0
> between preshea= ves are not morphisms in the category of functors=C2=A0
> C -&= gt; Sets^{op} but in the opposite category.

Ah, ri= ght. =C2=A0The reason why I defined presheaves this way is that=C2=A0
=
you can just say that the slice category over a presheaf $P$ is=C2=A0<= /div>
presheaves over the category of elements of $P$, rather than=C2= =A0
copresheaves, so it's more uniform and certain proofs bec= ome a=C2=A0
little bit nicer. =C2=A0Of course, one could start wi= th C^{op} and use=C2=A0
copresheaves throughout, but then I think= things would get quite=C2=A0
confusing with the Yoneda embedding= .

But thanks for pointing out this problem. =C2=A0= Somehow, it had never=C2=A0
occured to me that natural transforma= tions are going in the wrong=C2=A0
direction with my definition.<= /div>

Paolo

------=_Part_235_1699592489.1487947017752-- ------=_Part_234_1314358376.1487947017752--