From mboxrd@z Thu Jan 1 00:00:00 1970 X-Received: by 10.13.253.66 with SMTP id n63mr9196133ywf.41.1502703425453; Mon, 14 Aug 2017 02:37:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 10.36.94.207 with SMTP id h198ls3255043itb.5.canary-gmail; Mon, 14 Aug 2017 02:37:04 -0700 (PDT) X-Received: by 10.107.27.136 with SMTP id b130mr5080518iob.76.1502703424774; Mon, 14 Aug 2017 02:37:04 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1502703424; cv=none; d=google.com; s=arc-20160816; b=imprSS8z2Kiz6ExiXVfnuqfHzReVSlgngLWMw1BX3VA0f17KjeiOQDQejo2+2ii7Fn 2Ft748c+bVW290tVuMQXMTN+9K8glWXMIAzDHvvZvVfNBojYBzHVeqn9Ae6tlhdxKLBj mLd2pQEilzlK0hTgc5f5ugq/Om/ZPQmir9/nVsV/FfWtgNYaPES2bPllfTVdDvxuBM1L IP4hisal4OWyczSge5NYH/n5l0sGtp9yx7PxXVKdk+6IPv1ma9P4nHkUN9HY+3XyzsUF 6HpFiK0m2Kig5AfzQixwW8UYxNs/N3hK8KTU7S3A+r81HdX06qaSWW393bchm8xx2waq HNOQ== 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:sender:mime-version:dkim-signature :arc-authentication-results; bh=2c773UY/pOj9SKMHJk8DRhPNWAQ0cNuMEwC2NDnL3PQ=; b=03pZGBtLz9q2A0bxGwT1zq1V+jxnRFHxl7eem7iYh/MA4hIvdCka6JvOLvLD/+Ndrq /WX4+98oFbTxIGvIZqRDhm0qnH5QzwT6sGDt4KnEO6Kdl+igeY0bT9z+5QZsVxaElf7d qL59K0Eu/s3dap0RJN6zPOYC7tm3LXNaqXPYpfafzhITViteotGQhb2PatpMZX1JHeDe clxQe7vUSVbqxsA6I9IB/fQIMmkd5iyuAIlEp3yv42VLbkRdwpjUw5zEOc2eXf0jMBx/ XXsjubJoIDIOhxr2h03EqbgnzNtHlYJu61JtgoNQY9VB21JHNjYr/xJREYWvmZZJ41sJ KsPA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=AjJHQDi6; spf=pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:400d:c09::22d as permitted sender) smtp.mailfrom=andrew....@gmail.com Return-Path: Received: from mail-qk0-x22d.google.com (mail-qk0-x22d.google.com. [2607:f8b0:400d:c09::22d]) by gmr-mx.google.com with ESMTPS id x8si734871ywg.12.2017.08.14.02.37.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 14 Aug 2017 02:37:04 -0700 (PDT) Received-SPF: pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:400d:c09::22d as permitted sender) client-ip=2607:f8b0:400d:c09::22d; Authentication-Results: gmr-mx.google.com; dkim=pass head...@gmail.com header.s=20161025 header.b=AjJHQDi6; spf=pass (google.com: domain of andrew....@gmail.com designates 2607:f8b0:400d:c09::22d as permitted sender) smtp.mailfrom=andrew....@gmail.com Received: by mail-qk0-x22d.google.com with SMTP id x191so47351568qka.5 for ; Mon, 14 Aug 2017 02:37:04 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc:content-transfer-encoding; bh=2c773UY/pOj9SKMHJk8DRhPNWAQ0cNuMEwC2NDnL3PQ=; b=AjJHQDi6VyCELDbZxT1nMZnM2ubqb2O38lymyJvPfP35PS1C0xfPjPLUgWnNaqdoQ1 RQcWCxBlX2EcWC0oTlUrliRlimN4UedJtZcPSXnidy3zGb61jsur3GsOKiyS7CLnXKLz sWLD4a+IJtoslaV1tUjdXOGT1V4tzwwCWq1xzRjDmRKgvkeGL26OKIhcrPpfjtkCm+R2 GadtfWEMxcWNVCxL+U8Wqgk7wAq/vG7FLUpXXMJZu7FpSn36S5/h3f+VA9Ka0dZlqGOZ TvCCg071rDTpkn8mwsrBajoCzipB72tBdUf5u9W5SBcG3bO2f7E/uRftLu2lmzhwtpdc OPHw== X-Gm-Message-State: AHYfb5gzx6fdoshgqa2S8cq6yXPeGCAGGJDciL8rfxTVfHl5nA5UMVky X8Lk+cVAM6amQqqpxt6RnGqysZh3bw== X-Received: by 10.55.215.28 with SMTP id m28mr31526422qki.318.1502703424561; Mon, 14 Aug 2017 02:37:04 -0700 (PDT) MIME-Version: 1.0 Sender: andrew....@gmail.com Received: by 10.140.104.46 with HTTP; Mon, 14 Aug 2017 02:36:44 -0700 (PDT) In-Reply-To: References: <56a8e45f-6800-813b-b70e-c6776dd70869@gmail.com> From: Andrew Pitts Date: Mon, 14 Aug 2017 10:36:44 +0100 Message-ID: Subject: Re: [HoTT] univalence without coherent equivalences To: Michael Shulman Cc: "HomotopyT...@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On 14 August 2017 at 10:32, Michael Shulman wrote: > On Mon, Aug 14, 2017 at 2:29 AM, Andrew Pitts wr= ote: >> and replacing =E2=80=9Cevery equivalence=E2=80=9D by >> =E2=80=9Cevery isomorphism=E2=80=9D is nice (I had noticed that finesse = before), >> 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)? Oh, yes, quite right (note to self: think before you post!) Andy