From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.118.77 with SMTP id j13mr1024486ywk.33.1487949015100; Fri, 24 Feb 2017 07:10:15 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.110.142 with SMTP id w136ls640103itc.22.canary-gmail; Fri, 24 Feb 2017 07:10:14 -0800 (PST) X-Received: by 10.99.51.206 with SMTP id z197mr1119805pgz.88.1487949014417; Fri, 24 Feb 2017 07:10:14 -0800 (PST) Return-Path: Received: from pps5.ias.edu (pps5.ias.edu. [192.16.204.88]) by gmr-mx.google.com with ESMTPS id u30si908016ywh.7.2017.02.24.07.10.14 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 24 Feb 2017 07:10:14 -0800 (PST) Received-SPF: pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) client-ip=192.16.204.88; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of vlad...@ias.edu designates 192.16.204.88 as permitted sender) smtp.mailfrom=vlad...@ias.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=ias.edu Received: from pps.reinject (pps5.ias.edu [127.0.0.1]) by pps5.ias.edu (8.16.0.17/8.16.0.17) with ESMTPS id v1OFADKI004349 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Fri, 24 Feb 2017 10:10:13 -0500 Received: from pps5.ias.edu (pps5.ias.edu [127.0.0.1]) by pps.reinject (8.16.0.16/8.16.0.16) with SMTP id v1OFADk5004340; Fri, 24 Feb 2017 10:10:13 -0500 X-Proofpoint-Sentinel: stfjxMnNb3BXG3c9+LeH8KXrBVvAArwJ98Qt2Aj8meFVRd5TYWx0ZWRfXwUP RFQNuFVBVG+FWFBqsQPLrjjsSqBsgBXzBUeBKxRMRvJFIdvc9P/EBglgrV3G9UFIXqG2/q9SMLR9 UQ4Ivs0+IFrOfZt7Xg== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps5.ias.edu with ESMTP id v1OFADED004339 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Fri, 24 Feb 2017 10:10:13 -0500 Received: from pool-96-248-86-80.cmdnnj.fios.verizon.net ([96.248.86.80] helo=vladimirs-mbp-2.home) by imap.math.ias.edu with esmtpsa (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.80.1) (envelope-from ) id 1chHVd-0005y6-28; Fri, 24 Feb 2017 10:10:13 -0500 From: Vladimir Voevodsky Message-Id: Content-Type: multipart/alternative; boundary="Apple-Mail=_E248CC0C-9F4E-4BEA-8874-373E23D9E2CE" Mime-Version: 1.0 (Mac OS X Mail 10.2 \(3259\)) Subject: Re: [UniMath] Re: [HoTT] about the HTS Date: Fri, 24 Feb 2017 10:10:12 -0500 In-Reply-To: Cc: "Prof. Vladimir Voevodsky" , Homotopy Type Theory , benedik...@gmail.com, univalent-...@googlegroups.com To: Paolo Capriotti 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> X-Mailer: Apple Mail (2.3259) X-Proofpoint-Virus-Version: vendor=fsecure engine=2.50.10432:,, definitions=2017-02-24_10:,, signatures=0 X-Proofpoint-Spam-Reason: safe X-IAS-PPS-SPAM: NO X-Proofpoint-Spam-Details: rule=ias_safe policy=ias score=0 spamscore=0 suspectscore=0 malwarescore=0 phishscore=0 adultscore=0 bulkscore=0 classifier=donotscan adjust=0 reason=safe scancount=1 engine=8.0.1-1612050000 definitions=main-1702240148 X-IAS-PPS-PHISH: NO --Apple-Mail=_E248CC0C-9F4E-4BEA-8874-373E23D9E2CE Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 Our definition of the category of elements (cf. ElementsOp.v in UniMath/Uni= Math/Ktheory), and I think it is the standard one, is that morphisms are mo= rphisms f:X -> X=E2=80=99 such that p=3DP(f)(p=E2=80=99). Then all works a= s expected. > On Feb 24, 2017, at 10:06 AM, Paolo Capriotti wrote: >=20 > Vladimir Voevodsky writes: > > The slice category over P is equivalent to presheaves on the category o= f elements of P. What is your definition of the category of elements of $P$= ? Objects are pairs $(X:C,p:P(X))$, and morphisms from $(X,p)$ to $(X=E2=80= =99,p=E2=80=99)$ are=E2=80=A6? >=20 > ...morphisms $f : C(X',X)$ such that $Pf(p) =3D p'$. >=20 > The slice category of the category of functors $A -> Set$ over a functor = $F$ is equivalent to functors $el(F) -> Set$, right? Now if you define pre= sheaves as functors $C^{op} -> Set$, you get that presheaves on $C$ over a = presheaf $P$ are equivalent to *functors* $el(P) -> Set$, not presheaves on= $el(P)$. >=20 > That's why I was trying to be clever and use that unnatural definition of= presheaves, but, as you pointed out, that doesn't work either, because the= resulting category of presheaves is the opposite of what we want. >=20 > Paolo >=20 >=20 > --=20 > You received this message because you are subscribed to the Google Groups= "Univalent Mathematics" group. > To unsubscribe from this group and stop receiving emails from it, send an= email to univalent-mathem...@googlegroups.com . > To post to this group, send email to univalent-...@googlegroups.com . > Visit this group at https://groups.google.com/group/univalent-mathematics= . > To view this discussion on the web visit https://groups.google.com/d/msgi= d/univalent-mathematics/ebf61361-d581-4a25-98cf-0e345e2e2035%40googlegroups= .com . > For more options, visit https://groups.google.com/d/optout . --Apple-Mail=_E248CC0C-9F4E-4BEA-8874-373E23D9E2CE Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8 Our definition of = the category of elements (cf. ElementsOp.v in UniMath/UniMath/Ktheory), and= I think it is the standard one, is that morphisms are morphisms f:X -> = X=E2=80=99 such that  p=3DP(f)(p=E2=80=99). Then all works as expected= .


=
O= n Feb 24, 2017, at 10:06 AM, Paolo Capriotti <p.cap...@gmail.com> wrote:

Vladimir Voevodsky writes:
> The slice = category 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 = pairs $(X:C,p:P(X))$, and morphisms from $(X,p)$ to $(X=E2=80=99,p=E2=80=99= )$ are=E2=80=A6?

= ...morphisms $f : C(X',X)$ such that $Pf(p) =3D p'$.
<= br class=3D"">
The slice category of the category of f= unctors $A -> Set$ over a functor $F$ is equivalent to functors $el(F) -= > Set$, right?  Now if you define presheaves as functors $C^{op} -&= gt; Set$, you get that presheaves on $C$ over a presheaf $P$ are equivalent= to *functors* $el(P) -> Set$, not presheaves on $el(P)$.

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

Paolo


--
You received this message because you are subscribed to the Google Groups "= Univalent Mathematics" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = univalent-mathem...@googlegroups.com.
To post to this group, send email to univalent-...@googlegroups.com.
Visit this group at https://groups.google.com/group/univalent-mathematics= .
To view this discussion on the web visit https:= //groups.google.com/d/msgid/univalent-mathematics/ebf61361-d581-4a25-98cf-0= e345e2e2035%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--Apple-Mail=_E248CC0C-9F4E-4BEA-8874-373E23D9E2CE--