From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.36.34.149 with SMTP id o143mr4919199ito.29.1502703195192; Mon, 14 Aug 2017 02:33:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.107.58.197 with SMTP id h188ls4456954ioa.44.gmail; Mon, 14 Aug 2017 02:33:14 -0700 (PDT) X-Received: by 10.31.131.139 with SMTP id f133mr14110614vkd.13.1502703194567; Mon, 14 Aug 2017 02:33:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1502703194; cv=none; d=google.com; s=arc-20160816; b=TGGmJOCQUJiXWrz34dqi3fzqVGxbySVfT7sH2bcDtNfmqXdGUeuhnvMs+uoawIVTdJ EcDe0MOGNtxJ3yRfFN29qmqOpbHomJ0rPjYb46maSEf+ofFr3a4KQnY+EGzXsEwFPP+e CsQ40wYU3IFRY1DlrqU9kTysj/iL/5OTcS6thDX4TCZK6bNzYvXcq036eZ8Dqa0Vcw7m fiYfEAc38bKUcXrJBBpJ5l0MNs3bt3sW3be0ZTX/TbAFME3sPlXXvU+tFdU4t4YYIac2 eZf0KhLsLwG0uHDuKkH/LZi0a6d3ItC+HpA064laTUQU8t6poGVmb34hCobOmxaXZHSv xkAg== 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=NAlpyRsK4n0SVpsH+XiVDOC+6o/TfECr4PixIafBrXo=; b=DuDMK37ybwbomUkUyPSo9LGtI5VDMjUUAz4+kTBBoM5s6dM7c5xepaJX/TdWt31MUA NbKxcvqtv99rLKkU1Ig3h3olXCg4SJ1GTAxOgnqa4WR3DXdFmVyVy5D5ZsmsLJVj50xC 0R5ETUpuKrYex+vsjkb72/X+9VbZWC2/dGY8OLLxNN70BC5AmeBS2vBJrr6Pbvfx9zrZ PydsZwM+ETxo3mzvNFaK94b0GKq1LsZEu3purvdpCy/SXV+tv/WZ42hqYqIe8yinjSMi sjOTSj+hjq7QTmc74LFiS1S1K8mLSO3uNkpkN+buDadpH2uI+yrhzyOLvaz/PhdtqbLR z8eg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=c06kcti2; spf=neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Return-Path: Received: from mail-yw0-x230.google.com (mail-yw0-x230.google.com. [2607:f8b0:4002:c05::230]) by gmr-mx.google.com with ESMTPS id z134si777932ywd.8.2017.08.14.02.33.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 14 Aug 2017 02:33:14 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) client-ip=2607:f8b0:4002:c05::230; Authentication-Results: gmr-mx.google.com; dkim=pass head...@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=c06kcti2; spf=neutral (google.com: 2607:f8b0:4002:c05::230 is neither permitted nor denied by domain of shu...@sandiego.edu) smtp.mailfrom=shu...@sandiego.edu Received: by mail-yw0-x230.google.com with SMTP id l82so51533418ywc.2 for ; Mon, 14 Aug 2017 02:33:14 -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=NAlpyRsK4n0SVpsH+XiVDOC+6o/TfECr4PixIafBrXo=; b=c06kcti2p9OEjn6OXTtmbJ6t4o/h0lSqZ3gDkd6/MCZngHjmjaG7gaWeFmEToJ+ndY N8z0DGXPSG4T4hSWJiUIElxkDpMITrPorPbI8rFnV6VYhHsP+5ukqEPDVTadBR0sLTtW t5lXz3Q/q3RMucXRl2sqzinyyZq+OJ2qGMi0ZSWlOqnw/1BRtRrV95lC90td/s8fb80h raOm/pOIquWuHBcQSdZ6t6GvykZcz/Lyi8vV+ohueKdCqK916s7r/K78z99+f327rsGj LaagO0ZZg6bQHKBQuAhhFYwW8viumtfRdG0i9zPCvZp4SjfHb1DZTvltyNT8UFy5tHmL Lk6w== X-Gm-Message-State: AHYfb5imu2zmi+DrleZN6k0/pl68CwdsijbG5nud8HAdehRQUfzaVOsB I1vXbyEYBKJwYmaQAvY= X-Received: by 10.129.79.210 with SMTP id d201mr18905693ywb.467.1502703194239; Mon, 14 Aug 2017 02:33:14 -0700 (PDT) Return-Path: Received: from mail-yw0-f170.google.com (mail-yw0-f170.google.com. [209.85.161.170]) by smtp.gmail.com with ESMTPSA id s11sm2545065ywj.105.2017.08.14.02.33.13 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 14 Aug 2017 02:33:13 -0700 (PDT) Received: by mail-yw0-f170.google.com with SMTP id p68so51856583ywg.0 for ; Mon, 14 Aug 2017 02:33:13 -0700 (PDT) X-Received: by 10.37.219.148 with SMTP id g142mr19032548ybf.17.1502703193282; Mon, 14 Aug 2017 02:33:13 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.255.10 with HTTP; Mon, 14 Aug 2017 02:32:52 -0700 (PDT) In-Reply-To: References: <56a8e45f-6800-813b-b70e-c6776dd70869@gmail.com> From: Michael Shulman Date: Mon, 14 Aug 2017 02:32:52 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] univalence without coherent equivalences To: Andrew Pitts Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Mon, Aug 14, 2017 at 2:29 AM, Andrew Pitts wrot= e: > and replacing =E2=80=9Cevery equivalence=E2=80=9D by > =E2=80=9Cevery isomorphism=E2=80=9D is nice (I had noticed that finesse b= efore), > except for the fact that transport along an identification is in > general an equivalence rather than an iso. Transport along an identification is certainly an "isomorphism" too; isn't that just as easy to prove as that it's an equivalence (for any notion of coherent equivalence)?