From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.107.38.196 with SMTP id m187mr620363iom.63.1500487378524; Wed, 19 Jul 2017 11:02:58 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.101.129 with SMTP id u123ls4624300itb.2.gmail; Wed, 19 Jul 2017 11:02:57 -0700 (PDT) X-Received: by 10.98.62.207 with SMTP id y76mr612078pfj.52.1500487377806; Wed, 19 Jul 2017 11:02:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500487377; cv=none; d=google.com; s=arc-20160816; b=YdohnMJEPDnQktzOiYV6bbq/p80ArUgDr2IbwpzvJIhrnoGy1uCYRY45EwmtJDyMvP quMbWoXmsQRjOXtGmi/oKicmZQSmS+xAGmuTPP1q7r0F2F/VUV/fnA/VY2hQ0EZ7g2tX QHA6E4FfwBNnVSJpxr1SoVIvIUbPV6moMe/EDTilhpMxY4fnH9rDUKEhsf7mkKOIY6py 99kQm4JMwwUBTMX9WMf5GFiClg327X5uI2DJPS748VY+dc8A+B7bQHKrVhDsQIMtK+oZ gum1078RMMO3MQp1vMfAArv44cH2KrN9RmHWQtx3tORqVimS1r1Z16YRC3Ulyw8cSJP3 uY5w== 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:in-reply-to:references :mime-version:dkim-signature:arc-authentication-results; bh=JTIi7Ax/gdYRq9C/SaYQcUvUBtTqAtMgv0uUQ0nSsxE=; b=K47r1TNYFwvkStvOQn2xEWCwwdKId/5uwim2IlNVV2dxxxteX7YxgaS4DWmbAV+yhB 5O6qdQecez2L5cPSsCLvnrzX8g71uBzjpnl5InK+/0is0rjBJhL+KoliEKYrQMoNjJ2F EKDlQs74LI6d2xXvFra/ZxKB0CKhZikNA0RXSAujnWle5TwAPRm96DL8m0WHvNO9979I fFV9c1t2a0CJgfkSScF3ybHeeeOMuRre8g22iEESPlI/FPDRIya+MMY3e9citKiDF777 JGykyR+jC/TMA2vIU+l0iQFNv+py8tqaNnqfQDwLarJ9u/r3uv+xP9ZjxgFuPQpGLWdE 6Etg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=NMK2IGm8; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::230 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Return-Path: Received: from mail-qk0-x230.google.com (mail-qk0-x230.google.com. [2607:f8b0:400d:c09::230]) by gmr-mx.google.com with ESMTPS id d192si53331ywe.1.2017.07.19.11.02.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 19 Jul 2017 11:02:57 -0700 (PDT) Received-SPF: pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::230 as permitted sender) client-ip=2607:f8b0:400d:c09::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=NMK2IGm8; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c09::230 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qk0-x230.google.com with SMTP id t2so2236561qkc.1 for ; Wed, 19 Jul 2017 11:02:57 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=JTIi7Ax/gdYRq9C/SaYQcUvUBtTqAtMgv0uUQ0nSsxE=; b=NMK2IGm8bO90ZKgGgi9cOvwW/6d7ARjzBcMCr5EuWwmqye23zS5Fx1dC1+mFz639mW DsP3w1I9vIAFWfce111hHfEv5MR2ZiEoMXAm+IzpgEohIthAJ49Npm+LZ5qgcvatoDRY efz73hpafla0RnmHjVj7LVIbG01B/24rT8hh/uBXmrfuM7esXlOiRS6+CFOX8DcwDKwA nEx5vAl4y3A6E9SMDtz/Qm7bYw9yEA9eUmmhpq6+UufO2GUjaVZN0cTpTq4DYKc3vXhK KxJtk5L7+E1yRFTSqwGq9vxh793YVI7iLIGEBcjElddxaciYLHLMc1ybxsitS8DLCpYB uubA== X-Gm-Message-State: AIVw11258eBACuKXJoX25zWhYdOP2FrZGWLWHcKx2pIv3T8LcrPmnLwc oIp1GFSTWqJmiLoEGDtNl3zqPq7hW4DN X-Received: by 10.233.232.149 with SMTP id a143mr1270122qkg.339.1500487377293; Wed, 19 Jul 2017 11:02:57 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Jason Gross Date: Wed, 19 Jul 2017 18:02:46 +0000 Message-ID: Subject: Re: [HoTT] Weaker forms of univalence To: Michael Shulman Cc: Ian Orton , "HomotopyT...@googlegroups.com" Content-Type: multipart/alternative; boundary="94eb2c03e4421d14a70554af71a2" --94eb2c03e4421d14a70554af71a2 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable > I am not sure about (1). It might be an open > question even in the > case when A and B are propositions. If A and B are hProps, then (1) =3D> (3) under function extensionality (not sure if you can do away with out here). The key idea is that there can be only one equivalence between hProps. To prove contractibility, we must show that (A, idequiv) =3D (B, e) for any equivalence e of A and B. Let us prov= e A =3D B by (1); what remains is proving that idequiv =3D transport (1) e. = It now suffices to show that A =E2=89=83 A is an hProp for A an hProp. This f= ollows from function extensionality. On Wed, Jul 19, 2017, 8:28 PM Michael Shulman wrote: > I don't think you need function extensionality for contractibility and > Sigma to respect equivalence. We need funext for Pi to respect > equivalence, but there are no Pis here. > > On Wed, Jul 19, 2017 at 10:21 AM, Jason Gross > wrote: > > Certainly (2) =3D> (3), at least if you assume function extensionality;= it > > suffices to show that (\Sigma B, A =E2=89=83 B) is contractable, and si= nce > > contractibility and sigma respect equivalence, we can transfer the proo= f > > that (\Sigma B, A =3D B) is contractable. I think the same is not true = of > (1), > > though I'm not sure. > > > > On Wed, Jul 19, 2017, 7:26 PM 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. > > > > -- > > You received this message because you are subscribed to the Google Grou= ps > > "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. > --94eb2c03e4421d14a70554af71a2 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable

> I am not sure about (1).=C2=A0 It might be an open >= question even in the
> case when A and B are propositions.

If A and B are hProps, then (1) =3D> (3) under function e= xtensionality (not sure if you can do away with out here).=C2=A0 The key id= ea is that there can be only one equivalence between hProps. To prove contr= actibility, we must show that (A, idequiv) =3D (B, e) for any equivalence e= of A and B.=C2=A0 Let us prove A =3D B by (1); what remains is proving tha= t idequiv =3D transport (1) e.=C2=A0 It now suffices to show that A =E2=89= =83 A is an hProp for A an hProp.=C2=A0 This follows from function extensio= nality.


On Wed, Jul 19, 2017, 8:28 = PM Michael Shulman <shu...@sandie= go.edu> wrote:
I don't t= hink you need function extensionality for contractibility and
Sigma to respect equivalence.=C2=A0 We need funext for Pi to respect
equivalence, but there are no Pis here.

On Wed, Jul 19, 2017 at 10:21 AM, Jason Gross <jason...@gmail.com> wrote:
> Certainly (2) =3D> (3), at least if you assume function extensional= ity; it
> suffices to show that (\Sigma B, A =E2=89=83 B) is contractable, and s= ince
> contractibility and sigma respect equivalence, we can transfer the pro= of
> that (\Sigma B, A =3D B) is contractable. I think the same is not true= of (1),
> though I'm not sure.
>
> On Wed, Jul 19, 2017, 7:26 PM Ian Orton <ri...@cam.ac.uk> wrote:
>>
>> Consider the following three statements, for all types A and B: >>
>>=C2=A0 =C2=A0 (1)=C2=A0 (A =E2=89=83 B) -> (A =3D B)
>>=C2=A0 =C2=A0 (2)=C2=A0 (A =E2=89=83 B) =E2=89=83 (A =3D B)
>>=C2=A0 =C2=A0 (3)=C2=A0 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 hav= e (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/optou= t.
>
> --
> You received this message because you are subscribed to the Google Gro= ups
> "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.
--94eb2c03e4421d14a70554af71a2--