From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.99.97.87 with SMTP id v84mr636452pgb.224.1500485330496; Wed, 19 Jul 2017 10:28:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.88.208 with SMTP id f199ls9195747itb.18.canary-gmail; Wed, 19 Jul 2017 10:28:49 -0700 (PDT) X-Received: by 10.129.49.78 with SMTP id x75mr450938ywx.212.1500485329763; Wed, 19 Jul 2017 10:28:49 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500485329; cv=none; d=google.com; s=arc-20160816; b=kXuFGoYtvQAeozN7Yfcid5p7eSsMMA6+EFZ5EsVEccu1QrUNbfvKZWmXK0mb4zwgzL Fh2zSBV+TchXRFyjOcaW7PqNA0xDnaRaNDlOvD5yg9z5y4eBuQYZDzLGxTOPiflNOpYL LiO4k3DMv2OVGvtMY23BcU/d3S56a/Jv/zw2Om6R84dqO5lQ8edFHgnhe4oQ1JCJToff ocSRadWHeGmJ/qB7zVSSKyaYUCqX4ZDBc80913khR6qlWDDm5f/dMl11/tumlyB4cLmh u06VzLBxxKeFoVKoP9mrKmSywVWZfUW67fljTAAUyaxMFWS4MujM1je6nZd+zd4AxyW2 lYGg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:dkim-signature :arc-authentication-results; bh=BhyWa0LQRixNPm8cmaX34IxFJKWv5CMspgrQ8ImfgX4=; b=dfjSkanJPj80tIMq4WAznM8yHxH+Bv482MoVK5CUyiVK0THczlgvb/vlzqt6j7qM+R F4/lvkty/mgltfmdlzWaMqcYBCpYawQ802O3kU2sK45K4847kcDaIbJnuDIoXzdHh0Zi Li7ahBLAloCh3rkbdlE6QOX6884bdzGYoNCfYkM0SWJAhZhjPG8MuRgNnRM15FcqKUji hRvKEqWt1kOuWXTHgkVKYC+Ia4h9+1kkKT71Q+c1XA4VKIcS+nyiG6Ge6/NzbHI78OPz c141bYVlQlBnwDJrMrqyaPLPRoJmQzGrZBQCOYQOi6KEbcroJ+V0z4VrLXqmmdmN6kHL scMg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=PMiOBAsQ; spf=neutral (google.com: 2607:f8b0:4002:c05::22b is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x22b.google.com (mail-yw0-x22b.google.com. [2607:f8b0:4002:c05::22b]) by gmr-mx.google.com with ESMTPS id w67si43768ywg.11.2017.07.19.10.28.49 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 19 Jul 2017 10:28:49 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22b is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=PMiOBAsQ; spf=neutral (google.com: 2607:f8b0:4002:c05::22b is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x22b.google.com with SMTP id y186so3349775ywc.1 for ; Wed, 19 Jul 2017 10:28:49 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=sandiego-edu.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-transfer-encoding; bh=BhyWa0LQRixNPm8cmaX34IxFJKWv5CMspgrQ8ImfgX4=; b=PMiOBAsQeGPJZpqKlhomY9rqKigr+3x0j3d1ruHC+lRWi3Li1BVsho9fV3jTLbGGxM V4RPeWvq9xn8UMThcKA+f7CBQCJfXMOAX5xqRlvm7qhPzZC2b4LEHKb3qS92Vf4EARoi vOi0X6Egisai0ZwJFemQqLfu+20BcfHqHQr8DQaDuZ/ZradHqL5eWAa0s1zcr8LkciUL RA0BYasf+0pXZn/H7K2pOpLNX//EfSAorEOfgtQPDh7bLQNqS1X835liJj/9Nr5XdF3F zXuP2JftzKHAvUW6RX9VO5CHub73TFfF5eRrFyFVzF3pRr0BaKxLjiP8zFAMsn59iECE Gr9Q== X-Gm-Message-State: AIVw112U5IINu+cDo2VMUB+d6TdcVomQ3JiB5dUGvUGjsyN42UHRs3zP Z+8mNlwuvT2QrP+gscw= X-Received: by 10.13.235.198 with SMTP id u189mr750459ywe.360.1500485329139; Wed, 19 Jul 2017 10:28:49 -0700 (PDT) Return-Path: Received: from mail-yb0-f170.google.com (mail-yb0-f170.google.com. [209.85.213.170]) by smtp.gmail.com with ESMTPSA id r8sm173290ywl.39.2017.07.19.10.28.48 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 19 Jul 2017 10:28:48 -0700 (PDT) Received: by mail-yb0-f170.google.com with SMTP id z37so1743656ybh.1 for ; Wed, 19 Jul 2017 10:28:48 -0700 (PDT) X-Received: by 10.37.172.135 with SMTP id x7mr781326ybi.238.1500485328541; Wed, 19 Jul 2017 10:28:48 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.255.10 with HTTP; Wed, 19 Jul 2017 10:28:27 -0700 (PDT) In-Reply-To: References: From: Michael Shulman Date: Wed, 19 Jul 2017 10:28:27 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Weaker forms of univalence To: Jason Gross Cc: Ian Orton , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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; i= t > suffices to show that (\Sigma B, A =E2=89=83 B) is contractable, and sinc= e > 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 Group= s >> "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n >> 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 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.