From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.98.33.88 with SMTP id h85mr2829658pfh.27.1500573457247; Thu, 20 Jul 2017 10:57:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.65.132 with SMTP id b4ls1419634itd.6.canary-gmail; Thu, 20 Jul 2017 10:57:36 -0700 (PDT) X-Received: by 10.99.4.87 with SMTP id 84mr3097107pge.185.1500573456373; Thu, 20 Jul 2017 10:57:36 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1500573456; cv=none; d=google.com; s=arc-20160816; b=oO0HmVy+4AzWStsE2nlG3XBka2kw+hjZwDbbDEvsU3EbEW+p3z7hroBn4/RWQTENEN BYaVNCuwBIQ0tRk+5nsjbluQywpe6aKWApv1/8cH/YaYKIbHQtA+uQu5+LpdDkzNdaRo g+2fP2ynHtEZOUaZXHAyuFClb95pitrwejIJ73mZTOrvMrReNSEUsJfk8BVilzS6TjSu aUlAVTfUtZ0pfW6Kx0/zTbBGAoYo6LLikCz6ma0BDgqQRWdDO/aZUrqc4YWj6OOS4tNO LCmnQX4hl046lupPVa+lHPHCdA28hJ/eOSPAHqAZOtryFPff3qs/R7zw3zsUZeunfCh1 5e7g== 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=5d6ZsSey9SwMCJ+B+MEx3afCVkrO74yPh13wSVKabiE=; b=Pqycx04p2DHE5HluOKN3fC36J6I0CB9+AFHJesUZy8A6fhoWZ7U1imKdTMs2RViiFW 0TEUxL2fwDRX0SAysk1vlNNd/5LQHKUAIkwTbtYlwsiSHjMkY6vMw45SI/De/QbfdxrR 474bqDPFlhiJ8hQXPdQOql2oGGHe9/bUrTLI9v3uIlHQFcB9XAgmYJ/4i1JUp6NsPmMl gPK5Bkd9fziIXGXq8dSbuXmHk4A2DnALhxKre51JNNN5yUTFcDenr6VhopZ61WeiLiAS 4U2PUVTdTsNSxR3LvgK9ZwB87A1dfKX2Yd3kWYlKUCo3IN3FeIdzdXB2svvxXpzoQBL8 n4qg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=zvT/dczI; spf=neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yb0-x229.google.com (mail-yb0-x229.google.com. [2607:f8b0:4002:c09::229]) by gmr-mx.google.com with ESMTPS id l136si211419ywc.5.2017.07.20.10.57.36 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jul 2017 10:57:36 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c09::229; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.b=zvT/dczI; spf=neutral (google.com: 2607:f8b0:4002:c09::229 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yb0-x229.google.com with SMTP id x6so436100yba.2 for ; Thu, 20 Jul 2017 10:57:36 -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=5d6ZsSey9SwMCJ+B+MEx3afCVkrO74yPh13wSVKabiE=; b=zvT/dczIV37O2SU78PqjQEC2/LhdZ4bJLT5VuX4UmioKW7cpMMbSqzVfQ1JPxNmpIn HYvLg4nT/QeQtO0A5jGm0DY7NDRL5b0Ww5cNX/7MSih7J848ULZZJAlfHzEw4YtoUPCD 12eMNKMkG+P3mveuLAbsxE0B4sT7a+91sKQYQoNfB3zA0KJHijE1CjqGZBAWBwxta3Im KV9ANW5dA0NaT0ZXrgdlOqCaV4SPeVqSZrbPGEqA/NEe+V/UUQBdmvecTB+R/CzT0rbM QbTPZNbJZ84r+wq9pT9AdHZt4XTaxjWlfiVriAsVGmPRe3Sn7GveoI8BHI4HrFIjljnl ERRw== X-Gm-Message-State: AIVw11183P51dn+7nevK6GNxPyPVdeY4NlNP5ufOkpUw7zrGP/Pl44Dc bhJgCPT12ZPsUl0RGhk= X-Received: by 10.37.34.68 with SMTP id i65mr4112303ybi.191.1500573455795; Thu, 20 Jul 2017 10:57:35 -0700 (PDT) Return-Path: Received: from mail-yb0-f174.google.com (mail-yb0-f174.google.com. [209.85.213.174]) by smtp.gmail.com with ESMTPSA id f126sm1006956ywf.102.2017.07.20.10.57.35 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 20 Jul 2017 10:57:35 -0700 (PDT) Received: by mail-yb0-f174.google.com with SMTP id z37so8151392ybh.1 for ; Thu, 20 Jul 2017 10:57:35 -0700 (PDT) X-Received: by 10.37.164.34 with SMTP id f31mr3842672ybi.317.1500573455082; Thu, 20 Jul 2017 10:57:35 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.255.10 with HTTP; Thu, 20 Jul 2017 10:57:14 -0700 (PDT) In-Reply-To: <9971190E-3BFB-4ECC-ACFA-466D4936D838@cmu.edu> References: <9971190E-3BFB-4ECC-ACFA-466D4936D838@cmu.edu> From: Michael Shulman Date: Thu, 20 Jul 2017 10:57:14 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Weaker forms of univalence To: Steve Awodey Cc: Bas Spitters , Ian Orton , "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable 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 an= y 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 so= mething 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 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 w= rote: >>> 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, and >>> the fact that based path spaces are contractible. But the >>> contractibility of based path spaces also gives (2) -> (4), and hence >>> (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 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. >>> >>> -- >>> 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. >> >> -- >> 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.