From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.132.79 with SMTP id u76mr4312609ywf.64.1500622993745; Fri, 21 Jul 2017 00:43:13 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.20.6 with SMTP id 6ls2454407iou.7.gmail; Fri, 21 Jul 2017 00:43:13 -0700 (PDT) X-Received: by 10.237.36.141 with SMTP id t13mr4325983qtc.109.1500622992947; Fri, 21 Jul 2017 00:43:12 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500622992; cv=none; d=google.com; s=arc-20160816; b=HGmBC2RCM7jLnUOXC0PMZM3YEysCmnH2Y9IdNu/uWtlyABcyZ8Zfvbfn2/8wIB4Z8N ATe/Dqs8QLmlbIwKbHS1OjpVbaMVuJuHo16OLiWwJNMmOI2P5mdI/YkdsqDa2Cx769eV DOD+U6wu1GUprdcDQ4SIZQCi5llBvwjmLOSpCCt3deHIKix+EUS0Wl4VReAc5uO8lahN WPJtan2/x6giBQhnzKrrzuDXlg6XomI3G5BM3Tb9cxcGXwDf3gnG+Mn+d6gH09c6NJMq zRRcvsyyjl5sHDbOTZe3iDLXE69MIwfbgce2T+J/Cila9xhsHZfE9wu+K3JvkuhbjoEm pHrA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=GPmJrUoZfvD9fNy6S6ue5ra1b89EyM9U9VBcBtje4Xs=; b=cxZXqNsaOgftCUQNHCvilkdD78BEXnjhh3PR2zFf/TItWamfjWy5TozX6MzCGMsG5b CEEAmGHPy/krYLHhFc364aTjU4q7l/IQQ6T5zoekbxWAYJmQ9wUGZM3vvqO3QmjDI6Yz V+tQb/421Qga002lcaV5EHLJ0LnEbHZgbq2irJxymae5iKUjFWRrrM4avuPnHxbbLFms QvZ7NvPD3xOSTLzpztjJRROzdyEkhciXhVDhlDYJX3DJZVbUEIvsgDwkX0jk1KTsTyNC mnx00+FgoOEG88nSPusedzpVT311LeFZiZBc/ZOOvmoB4HXFCNjQSscxtzg6VSGjRMKs 9H7w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=BL5zWe/v; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::230 as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-ua0-x230.google.com (mail-ua0-x230.google.com. [2607:f8b0:400c:c08::230]) by gmr-mx.google.com with ESMTPS id x191si215897vkx.4.2017.07.21.00.43.12 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 21 Jul 2017 00:43:12 -0700 (PDT) Received-SPF: pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::230 as permitted sender) client-ip=2607:f8b0:400c:c08::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=BL5zWe/v; spf=pass (google.com: domain of p.l.lu...@gmail.com designates 2607:f8b0:400c:c08::230 as permitted sender) smtp.mailfrom=p.l.lu...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-ua0-x230.google.com with SMTP id q25so20891128uah.1 for ; Fri, 21 Jul 2017 00:43:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=GPmJrUoZfvD9fNy6S6ue5ra1b89EyM9U9VBcBtje4Xs=; b=BL5zWe/vu1E5jTQITt9BNkOygVTDWAUlPz/A//79luzQ/Db3RNAiSQR5cj0qhNZgCh Zq6xmpfVmSPSPZ0PMA7dP21k0M3M+IEsCNTObbOrRDp17vnosDohGyj5MB3zinxATTpN nCIt9ThsBAR59EHNgcHlBcHhhnyhAJSZLaFSXhMpoLQMegz0Qds3cSzmViogaYLngjeZ evYg4I4YTiUp7xZlK6ScFva95RGTW5pNIGmePlCDR1wO0hHqfL6RlfRxNH8sbsfSOMB6 /VxKNnSWIuOfT0OFd/FCDHBlgw87xD0MNpxzvvN4meor0diLJneXY/Q6nz03Z73VEFP9 VhbA== X-Gm-Message-State: AIVw110Jqe+YB0GR8jY3FrJvgbyY2IMPtZ5bOQKCibu8uyrM7FJMnxwn JAbYwvw+/hrUw/7euYYHfwvuCZW7xw== X-Received: by 10.31.11.10 with SMTP id 10mr3346740vkl.199.1500622992745; Fri, 21 Jul 2017 00:43:12 -0700 (PDT) MIME-Version: 1.0 Received: by 10.176.91.142 with HTTP; Fri, 21 Jul 2017 00:43:12 -0700 (PDT) In-Reply-To: <7cf42606-2ef4-4575-ad0e-da78e2bca514@googlegroups.com> References: <9971190E-3BFB-4ECC-ACFA-466D4936D838@cmu.edu> <7cf42606-2ef4-4575-ad0e-da78e2bca514@googlegroups.com> From: Peter LeFanu Lumsdaine Date: Fri, 21 Jul 2017 08:43:12 +0100 Message-ID: Subject: Re: [HoTT] Weaker forms of univalence To: Matt Oliveri Cc: Homotopy Type Theory , Steve Awodey , Bas Spitters , Ian Orton Content-Type: multipart/alternative; boundary="001a114586426ca9f90554cf04ad" --001a114586426ca9f90554cf04ad Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Fri, Jul 21, 2017 at 2:36 AM, Matt Oliveri wrote: > Why wouldn't a skeletal LCCC be a model of (1) + UIP? > Because (1) would require not just the category itself to be skeletal, but also its slices, if =E2=80=9C(A =E2=89=83 B) -> (A =3D B)=E2=80=9D is taken= as a global axiom scheme, and unlike for skeletality of the category itself, one cannot generally replace a category by an equivalent one with suitably skeletal slices. (If it=E2=80=99s taken as a quantified axiom =E2=80=9Cforall A,B:U, (A =E2= =89=83 B) -> (A =3D B)=E2=80=9D, as it more usually is, then its validity doesn=E2=80=99t follow directly from = any amount of skeletality at all, but is to do with the specific universe chosen.) =E2=80=93p. > > On Thursday, July 20, 2017 at 1:57:37 PM UTC-4, Michael Shulman wrote: >> >> But is it known that this is definitely weaker? E.g. are there models >> that satisfy invariance but not the computation rule? >> >> On Thu, Jul 20, 2017 at 4:59 AM, Steve Awodey wrote: >> > I think we=E2=80=99ve been through this before: >> > >> > (1) (A =E2=89=83 B) -> (A =3D B) >> > >> > is logically equivalent to what may be called =E2=80=9Cinvariance=E2= =80=9D: >> > >> > if P(X) is any type depending on a type variable X, then given >> any equivalence e : A =E2=89=83 B , we have P(A) =E2=89=83 P(B). >> > >> > if we add to this a certain =E2=80=9Ccomputation rule=E2=80=9D, we get= something >> logically equivalent to UA: >> > assume p : A =E2=89=83 B =E2=86=92 A =3D B; then given e : A =E2=89=83= B, we have p(e) : A =3D B is >> a path in U. >> > Since we can transport along this path in any family of types over U, >> and transport is always an equivalence, >> > there is a transport p(e)=E2=88=97 : A =E2=89=83 B in the identity fam= ily. >> > The required =E2=80=9Ccomputation rule=E2=80=9D states that p(e)=E2=88= =97 =3D e. >> > >> > Steve >> > >> > >> > >> >> On Jul 20, 2017, at 8:56 AM, Bas Spitters >> wrote: >> >> >> >>> It was observed previously on this list, >> >> Maybe we should be using our wiki more? >> >> https://ncatlab.org/homotopytypetheory/ >> >> >> >> >> >> On Wed, Jul 19, 2017 at 7:19 PM, Michael Shulman >> wrote: >> >>> It was observed previously on this list, I think, that full >> univalence >> >>> (3) is equivalent to >> >>> >> >>> (4) forall A, IsContr( Sigma(B:U) (A =E2=89=83 B) ). >> >>> >> >>> This follows from the fact that a fiberwise map is a fiberwise >> >>> equivalence as soon as it induces an equivalence on total spaces, an= d >> >>> the fact that based path spaces are contractible. But the >> >>> contractibility of based path spaces also gives (2) -> (4), and henc= e >> >>> (2) -> (3). >> >>> >> >>> I am not sure about (1). It might be an open question even in the >> >>> case when A and B are propositions. >> >>> >> >>> >> >>> On Wed, Jul 19, 2017 at 9:26 AM, Ian Orton wrote: >> >>>> Consider the following three statements, for all types A and B: >> >>>> >> >>>> (1) (A =E2=89=83 B) -> (A =3D B) >> >>>> (2) (A =E2=89=83 B) =E2=89=83 (A =3D B) >> >>>> (3) isEquiv idtoeqv >> >>>> >> >>>> (3) is the full univalence axiom and we have implications (3) -> (2= ) >> -> (1), >> >>>> but can we say anything about the other directions? Do we have (1) >> -> (2) or >> >>>> (2) -> (3)? Can we construct models separating any/all of these >> three >> >>>> statements? >> >>>> >> >>>> Thanks, >> >>>> Ian >> > -- > You received this message because you are subscribed to the Google Groups > "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to HomotopyTypeThe...@googlegroups.com. > For more options, visit https://groups.google.com/d/optout. > --001a114586426ca9f90554cf04ad Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
On Fri, Jul 21, 2017 at 2:36 AM= , Matt Oliveri <atm...@gmail.com> wrote:
Why wouldn't a skeletal LCC= C be a model of (1) + UIP?

Because (1) wou= ld require not just the category itself to be skeletal, but also its slices= , if =E2=80=9C(A =E2=89=83 B= ) -> (A =3D B)=E2=80=9D is taken as a global axiom scheme,=C2=A0<= span style=3D"font-size:12.800000190734863px">and unlike for skeletality of= the category itself, one cannot generally replace a category by an equival= ent one with suitably skeletal slices.

(If it=E2=80=99s taken as a quantifi= ed axiom =E2=80=9Cforall A,B:U,=C2=A0(A =E2=89=83 B) -> (A =3D B)=E2=80=9D, as it more usuall= y is, then its validity doesn=E2=80=99t follow directly from any amount of = skeletality at all, but is to do with the specific universe chosen.)=

=
=E2=80=93p.

=C2=A0<= /div>

On Thursd= ay, July 20, 2017 at 1:57:37 PM UTC-4, Michael Shulman wrote:But is it known that this is definitely we= aker?=C2=A0 E.g. are there models
that satisfy invariance but not the computation rule?

On Thu, Jul 20, 2017 at 4:59 AM, Steve Aw= odey <awo...@cmu.edu> wrote:
> I think we=E2=80=99ve been through this before:
>
> =C2=A0(1) =C2=A0(A =E2=89=83 B) -> (A =3D B)
>
> is logically equivalent to what may be called =E2=80=9Cinvariance= =E2=80=9D:
>
> =C2=A0 =C2=A0 =C2=A0 =C2=A0 if P(X) is any type depending on a typ= e variable X, then given any equivalence e : A =E2=89=83 B , we have P(A) = =E2=89=83 P(B).
>
> if we add to this a certain =E2=80=9Ccomputation rule=E2=80=9D, we= get something logically equivalent to UA:
> assume p : A =E2=89=83 B =E2=86=92 A =3D B; then given e : A =E2= =89=83 B, we have p(e) : A =3D B is a path in U.
> Since we can transport along this path in any family of types over= U, and transport is always an equivalence,
> there is a transport p(e)=E2=88=97 : A =E2=89=83 B in the identity= family.
> The required =E2=80=9Ccomputation rule=E2=80=9D states that p(e)= =E2=88=97 =3D e.
>
> Steve
>
>
>
>> On Jul 20, 2017, at 8:56 AM, Bas= Spitters <b.a.w...@gmail.com> wrote:
>>
>>> It was observed previously on this list,
>> Maybe we should be using our wiki more?
>> https://ncatlab.org/homotopytypetheory/
>>
>>
>> On Wed, Jul 19, 2017 at 7:19 PM,= Michael Shulman <shu...@sandiego.edu> wrote:
>>> It was observed previously on this list, I think, that ful= l univalence
>>> (3) is equivalent to
>>>
>>> (4) =C2=A0forall A, IsContr( Sigma(B:U) (A =E2=89=83 B) ).
>>>
>>> This follows from the fact that a fiberwise map is a fiber= wise
>>> equivalence as soon as it induces an equivalence on total = spaces, and
>>> the fact that based path spaces are contractible.=C2=A0 Bu= t the
>>> contractibility of based path spaces also gives (2) -> = (4), and hence
>>> (2) -> (3).
>>>
>>> I am not sure about (1).=C2=A0 It might be an open questio= n even in the
>>> case when A and B are propositions.
>>>
>>>
>>> On Wed, Jul 19, 2017 at 9:26= AM, Ian Orton <ri...@cam.ac.uk> wrote:
>>>> Consider the following three statements, for all types= A and B:
>>>>
>>>> =C2=A0(1) =C2=A0(A =E2=89=83 B) -> (A =3D B)
>>>> =C2=A0(2) =C2=A0(A =E2=89=83 B) =E2=89=83 (A =3D B)
>>>> =C2=A0(3) =C2=A0isEquiv idtoeqv
>>>>
>>>> (3) is the full univalence axiom and we have implicati= ons (3) -> (2) -> (1),
>>>> but can we say anything about the other directions? Do= we have (1) -> (2) or
>>>> (2) -> (3)? Can we construct models separating any/= all of these three
>>>> statements?
>>>>
>>>> Thanks,
>>>> Ian

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsub...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

--001a114586426ca9f90554cf04ad--