From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.129.123.133 with SMTP id w127mr460048ywc.76.1500484883996; Wed, 19 Jul 2017 10:21:23 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.112.197 with SMTP id f188ls5293699itc.20.canary-gmail; Wed, 19 Jul 2017 10:21:23 -0700 (PDT) X-Received: by 10.98.201.1 with SMTP id k1mr523687pfg.13.1500484883169; Wed, 19 Jul 2017 10:21:23 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500484883; cv=none; d=google.com; s=arc-20160816; b=zwuOBgq8le9b5zdg6PR935xKQgbFelH51DigIxP/hGU2gNzQ1AL84VO2psUexsM/iy a46spLh46iZH6ccLbhiQQNj7VcRXDaFzjOR0H3Qn5h+0yjdg1VhHViItgCgl1DuuQDid fvTbpJpsfb3VTj3DNjp3vhqPAGECGwOr2MDUU6Pp9VzjgW3qeW1sgEU6T15Szr4QWIXm PpGquAutR1gkFgpevKw0a88eR5jTfogGcOgVSIK72i/zBIE5U7zFtTB7pB4cRGCPQMFc VGSEoUOb+swTlC/i9tYMCTNi+1CjUsm5q209hiRtMDIu9o0PFZftveBrSy7GaY0Kp1zV UnPw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature:arc-authentication-results; bh=0B2uqJXCIs5vvFS46KpMMEu3RBpl5le41dPppTjlYVo=; b=DfJyuspNQvanxq9UG2JKirt6MqM3nx8AfS36a9qOdlUSRoMKbpo6uGoi7kPZ5aHAHO JDqAXRsff5E+KPtu5LLsuM4HfyeProvwalUmB0Q4PANq64qfku+u3uw7RtQQ0RN54vKn 7EIOGiNFnUHJPnphDysbu3nkQa+Gz8jXa6NCzV4LrlFL5si+oVvwwpuzzMtrAG6HlMr2 DL6oJCpPNkDhBztF7SfFTd2M1xY9avIoN9tzx/Y9y9aMarCfFfvQSuHt9V+1xAERR7xN 6vq0PGAxAgS1RERVA0cJ7GTMdwspWjpPv8rc3/Xzk8g2exRTDqMYNqDjzm8nxFK4sOzB nyiw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.b=SF0TeABC; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c0d::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-qt0-x230.google.com (mail-qt0-x230.google.com. [2607:f8b0:400d:c0d::230]) by gmr-mx.google.com with ESMTPS id u128si46178ywg.4.2017.07.19.10.21.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 19 Jul 2017 10:21:23 -0700 (PDT) Received-SPF: pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c0d::230 as permitted sender) client-ip=2607:f8b0:400d:c0d::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.b=SF0TeABC; spf=pass (google.com: domain of jason...@gmail.com designates 2607:f8b0:400d:c0d::230 as permitted sender) smtp.mailfrom=jason...@gmail.com; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gmail.com Received: by mail-qt0-x230.google.com with SMTP id n42so7318058qtn.0 for ; Wed, 19 Jul 2017 10:21:23 -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; bh=0B2uqJXCIs5vvFS46KpMMEu3RBpl5le41dPppTjlYVo=; b=SF0TeABCAcCXKz+2z9NDIjZP5ZCNcs3wWiPTmZ3kCX5pxUsteXejYgrv+FJEf6m9gF eyOdUuHAEkD5dXS+296lHqkzzGftYU5ysOB1nG7ZgnUWKG7u7pXHg6JM3P7Z4o9JrzC1 Udv/DHVtaJsd9KhH62ZveXodA/bx/fszibY8fN15pQl+Ay/PRev/0QjIx0cQkdrM2A4V mbp2pD5bUs5SFw0C9cgH7n8QA5YpNVrxKyiiePSMNLQfJxPRrr37tRqq6MqvZAgnQPZs buLiuPfVUWL1qoa0U2Rn/GUVOUD1xEAQ9l3FDirCgQqreOiR9d7pHZdwy9hOf89IMiE5 exyw== X-Gm-Message-State: AIVw113qrVZI7huLyZ/L5pOyIcOVm83Nlaf75j94DINjLdfNl2tVT1ez xTr1qhvlqp4Yy8hjiN+AHuuo3Gt0SA== X-Received: by 10.200.51.150 with SMTP id c22mr1074332qtb.339.1500484882677; Wed, 19 Jul 2017 10:21:22 -0700 (PDT) MIME-Version: 1.0 References: In-Reply-To: From: Jason Gross Date: Wed, 19 Jul 2017 17:21:12 +0000 Message-ID: Subject: Re: [HoTT] Weaker forms of univalence To: Ian Orton , HomotopyT...@googlegroups.com Content-Type: multipart/alternative; boundary="001a1149d0406c43b90554aedc9d" --001a1149d0406c43b90554aedc9d Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 since contractibility and sigma respect equivalence, we can transfer the proof 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. > --001a1149d0406c43b90554aedc9d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Certainly (2) =3D> (3), at least if you assume function= extensionality; it suffices to show that (\Sigma B, A =E2=89=83 B) is cont= ractable, and since contractibility and sigma respect equivalence, we can t= ransfer the proof that (\Sigma B, A =3D B) is contractable. I think the sam= e is not true of (1), though I'm not sure.

On Wed, Jul 19, 2017= , 7:26 PM Ian Orton <ri...@cam.ac.uk<= /a>> wrote:
Consider the followi= ng 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) -&g= t;
(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 HomotopyTypeThe...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
--001a1149d0406c43b90554aedc9d--