From mboxrd@z Thu Jan  1 00:00:00 1970
Date: Fri, 24 Feb 2017 07:06:41 -0800 (PST)
From: Paolo Capriotti <p.cap...@gmail.com>
To: Homotopy Type Theory <HomotopyT...@googlegroups.com>
Cc: vlad...@ias.edu, benedik...@gmail.com,
	univalent-...@googlegroups.com,
	homotopyt...@googlegroups.com
Message-Id: <ebf61361-d581-4a25-98cf-0e345e2e2035@googlegroups.com>
In-Reply-To: <FAECD168-CDCC-4DC2-8968-3CEB59D26E71@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> <87k28fek09.fsf@capriotti.io>
 <FAECD168-CDCC-4DC2-8968-3CEB59D26E71@ias.edu>
Subject: Re: [UniMath] Re: [HoTT] about the HTS
MIME-Version: 1.0
Content-Type: multipart/mixed; 
	boundary="----=_Part_259_552548430.1487948801043"

------=_Part_259_552548430.1487948801043
Content-Type: multipart/alternative; 
	boundary="----=_Part_260_639369971.1487948801043"

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

Vladimir Voevodsky writes:
> The slice category over P is equivalent to presheaves on the category of=
=20
elements of P. What is your definition of the category of elements of $P$?=
=20
Objects are pairs $(X:C,p:P(X))$, and morphisms from $(X,p)$ to $(X=E2=80=
=99,p=E2=80=99)$=20
are=E2=80=A6?

...morphisms $f : C(X',X)$ such that $Pf(p) =3D p'$.

The slice category of the category of functors $A -> Set$ over a functor=20
$F$ is equivalent to functors $el(F) -> Set$, right?  Now if you define=20
presheaves as functors $C^{op} -> Set$, you get that presheaves on $C$ over=
=20
a presheaf $P$ are equivalent to *functors* $el(P) -> Set$, not presheaves=
=20
on $el(P)$.

That's why I was trying to be clever and use that unnatural definition of=
=20
presheaves, but, as you pointed out, that doesn't work either, because the=
=20
resulting category of presheaves is the opposite of what we want.

Paolo


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

<div dir=3D"ltr"><div>Vladimir Voevodsky writes:</div><div>&gt; The slice c=
ategory over P is equivalent to presheaves on the category of elements of P=
. What is your definition of the category of elements of $P$? Objects are p=
airs $(X:C,p:P(X))$, and morphisms from $(X,p)$ to $(X=E2=80=99,p=E2=80=99)=
$ are=E2=80=A6?</div><div><br></div><div>...morphisms $f : C(X&#39;,X)$ suc=
h that $Pf(p) =3D p&#39;$.</div><div><br></div><div>The slice category of t=
he category of functors $A -&gt; Set$ over a functor $F$ is equivalent to f=
unctors $el(F) -&gt; Set$, right? =C2=A0Now if you define presheaves as fun=
ctors $C^{op} -&gt; Set$, you get that presheaves on $C$ over a presheaf $P=
$ are equivalent to *functors* $el(P) -&gt; Set$, not presheaves on $el(P)$=
.</div><div><br></div><div>That&#39;s why I was trying to be clever and use=
 that unnatural definition of presheaves, but, as you pointed out, that doe=
sn&#39;t work either, because the resulting category of presheaves is the o=
pposite of what we want.</div><div><br></div><div>Paolo</div><div><br></div=
></div>
------=_Part_260_639369971.1487948801043--

------=_Part_259_552548430.1487948801043--