From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.31.192.13 with SMTP id q13mr43080445vkf.0.1473321585733; Thu, 08 Sep 2016 00:59:45 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.157.37.79 with SMTP id j15ls2214598otd.30.gmail; Thu, 08 Sep 2016 00:59:45 -0700 (PDT) X-Received: by 10.157.19.17 with SMTP id f17mr44370548ote.33.1473321585207; Thu, 08 Sep 2016 00:59:45 -0700 (PDT) Return-Path: Received: from mail-oi0-x22b.google.com (mail-oi0-x22b.google.com. [2607:f8b0:4003:c06::22b]) by gmr-mx.google.com with ESMTPS id f133si125143ita.1.2016.09.08.00.59.45 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 08 Sep 2016 00:59:45 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:4003:c06::22b as permitted sender) client-ip=2607:f8b0:4003:c06::22b; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com; spf=pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:4003:c06::22b as permitted sender) smtp.mailfrom=andrew....@gmail.com Received: by mail-oi0-x22b.google.com with SMTP id y2so60495779oie.0 for ; Thu, 08 Sep 2016 00:59:45 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc:content-transfer-encoding; bh=bOf448q6QS4oLhtqXDilNdeqqvX0sUUacxJ5wVOiFOM=; b=Sms87M1gsvfJzmsQZpE3zaVcSRa7Q0ozRzgpOeHCf/iMkk8YnNAoC7vrdPxERfPWVC 0UIunXcFOOXnCNBvo3cBR+4EjlEzGRLu+CqeOnbR2TzLaCfwhDNe8s6gBODZTTpuygOW +tXPB7j0u2DDvko4GNFoLliSuqQZFlBrj8uxuV/GMGYuA5RHKpZ6uoMUF5CPtLNqvB2x PmBvIVe21U9wmxQ1XSnvGIBqYoAFSkqBHG8qMU1b6tZpLb/0OmvDAUWehxsCCLbvWGBZ G/5y/3eJ4Z5feyJI16jVfHhVWPzvVLbJJoUBexrqsqWeuy5DeRtuMkacCWDsA1ztSW27 Ugvg== X-Gm-Message-State: AE9vXwNgNdkNmycGDD5v6/mYnyG8JCdj16/vVybguPzEFNymU9MXiWZfPy1Foj7nsoj9DWpPqSO7KwDCqgv9Ww== X-Received: by 10.157.43.87 with SMTP id f23mr9072377otd.83.1473321584974; Thu, 08 Sep 2016 00:59:44 -0700 (PDT) MIME-Version: 1.0 Sender: andrew....@gmail.com Received: by 10.202.218.130 with HTTP; Thu, 8 Sep 2016 00:59:24 -0700 (PDT) In-Reply-To: <227407CD-EB5C-4F5A-8D3E-B49C583D2CFE@cs.cmu.edu> References: <9F0041A0-328D-4C4F-8152-3E42305D372E@cs.cmu.edu> <227407CD-EB5C-4F5A-8D3E-B49C583D2CFE@cs.cmu.edu> From: Andrew Pitts Date: Thu, 8 Sep 2016 08:59:24 +0100 Message-ID: Subject: Re: [HoTT] weak univalence with "beta" implies full univalence To: Dan Licata Cc: Homotopy Type Theory , "Prof. Andrew M Pitts" Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On 7 September 2016 at 23:20, Dan Licata wrote: >> Also I think you need to assume the identity types, >> whatever they are, satisfy function extensionality don't you? > > I didn=E2=80=99t, but I stated ua=CE=B2 as an equation at function type. = If it were pointwise, then I would have needed it. For an identity type w= ith definitional J-on-refl reduction, this suffices to get the usual statem= ent of univalence (I updated the file a little to remove a use a funext to = make sure). Maybe this depends on having definitional J-on-refl though. OK, I see. The proof I made up for myself used along the way the fact that being contractible is a mere proposition; and for that I seemed to need function extensionality. But in any case, stating ua=CE=B2 pointwise seems more useful. Plus the fact that in the models where we have been using this nice characterisation of univalence, function extensionality holds for the propositional identity types in question for other reasons to do with them being given by paths, as you know. Best wishes, Andy