From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.157.41.66 with SMTP id d60mr983766otb.113.1487947013353; Fri, 24 Feb 2017 06:36:53 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.30.168 with SMTP id n37ls6652905otn.25.gmail; Fri, 24 Feb 2017 06:36:53 -0800 (PST) X-Received: by 10.157.56.136 with SMTP id p8mr983490otc.56.1487947012982; Fri, 24 Feb 2017 06:36:52 -0800 (PST) Return-Path: Received: from pps4.ias.edu (pps4.ias.edu. [192.16.204.92]) by gmr-mx.google.com with ESMTPS id r6si710519ywb.6.2017.02.24.06.36.52 (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 24 Feb 2017 06:36:52 -0800 (PST) Received-SPF: pass (google.com: domain of vlad...@ias.edu designates 192.16.204.92 as permitted sender) client-ip=192.16.204.92; Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of vlad...@ias.edu designates 192.16.204.92 as permitted sender) smtp.mailfrom=vlad...@ias.edu; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=ias.edu Received: from pps.reinject (pps4.ias.edu [127.0.0.1]) by pps4.ias.edu (8.16.0.17/8.16.0.17) with ESMTPS id v1OEao80002477 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Fri, 24 Feb 2017 09:36:50 -0500 Received: from pps4.ias.edu (pps4.ias.edu [127.0.0.1]) by pps.reinject (8.16.0.16/8.16.0.16) with SMTP id v1OEao1u002471; Fri, 24 Feb 2017 09:36:50 -0500 X-Proofpoint-Sentinel: stfjVmVt1d8tf0tNkU2Ez3FBMuGXL0ydI45AlLmM/9elMElTYWx0ZWRfX64N ADbKU6EjgExBhfUPwpEnS0Js+CqMSTgQ6fBUZQOQNf4Ncw+8Va92B5+tssz1ypzJHJ/rSKp6BBe+ UNX/rVlpWoNLeVVajg== Received: from imap.math.ias.edu (f5-bip.net.ias.edu [172.16.13.241]) by pps4.ias.edu with ESMTP id v1OEaoO8002470 (version=TLSv1.2 cipher=ECDHE-RSA-AES256-GCM-SHA384 bits=256 verify=NOT); Fri, 24 Feb 2017 09:36:50 -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 1chGzK-000501-Cw; Fri, 24 Feb 2017 09:36:50 -0500 Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 10.2 \(3259\)) Subject: Re: [UniMath] Re: [HoTT] about the HTS From: Vladimir Voevodsky In-Reply-To: <87k28fek09.fsf@capriotti.io> Date: Fri, 24 Feb 2017 09:36:49 -0500 Cc: "Prof. Vladimir Voevodsky" , Benedikt Ahrens , Univalent Mathematics , homotopytypetheory Content-Transfer-Encoding: quoted-printable Message-Id: 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> To: Paolo Capriotti 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-1702240142 X-IAS-PPS-PHISH: NO The slice category over P is equivalent to presheaves on the category of el= ements of P. What is your definition of the category of elements of $P$? Ob= jects 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? > On Feb 24, 2017, at 9:33 AM, Paolo Capriotti wrote: >=20 >>> On Feb 23, 2017, at 1:52 PM, Benedikt Ahrens wro= te: >>> Section 1.4.8 "Equality" gives an informal account and points to severa= l >>> precise definitions. >>> On page 43 two equality types are considered, one intensional one and >>> one with reflection rule. >=20 > I haven't actually considered something like what Vladimir suggested, tho= ugh. In the systems that I described in my thesis, exact equality is defin= ed for every type. >=20 > 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 opp= osite category. >=20 > 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 unifor= m 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. >=20 > 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. >=20 > Paolo >=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/87k28fek09.fsf%40capriotti.io. > For more options, visit https://groups.google.com/d/optout.