From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.1 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lf1-x137.google.com (mail-lf1-x137.google.com [IPv6:2a00:1450:4864:20::137]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id ad4a0025 for ; Wed, 18 Sep 2019 15:42:50 +0000 (UTC) Received: by mail-lf1-x137.google.com with SMTP id o9sf20725lfd.7 for ; Wed, 18 Sep 2019 08:42:50 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568821370; cv=pass; d=google.com; s=arc-20160816; b=kS0ZyZKYeBEZKnxMBnjUraqltw3mHrc238iM41KFJOXW89bzTQk/0yjSWdo+Gkm35Y aGP15h8C7f5Zl0JcB9A2BnBm0lx8+9SEQgEzizTKsmX0bQ7FTNVMiizp+gHPL4oM4mZv KXbfNZfKfjeERZiJSi1qigf2o3TPFkwV8j/tqpGw9ahBAe3h5h8z+AW4hlLamZ0jmILj wyGFmuFK7NZSo8iBL/khTmEEr3lvisYVqi8ChecPJ2UGkbFzkvMpbOmqZypRhEVRsjD9 /Dj4hEN2d/gO6cbiOYLzFI3IKWWTn9qT/OZIhJ8bvQ6RY49A8nHJdfu0nNvoeDTM/FiA CAqw== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=list-unsubscribe:list-archive:list-help:list-post:list-id :mailing-list:precedence:to:subject:message-id:date:from :mime-version:sender:dkim-signature; bh=+C/tfX7vT1mOdP4O80ejBhV08ZLnkT4XkjEN3CMWzbI=; b=IkNdJsTgzvaPA4OOaX9PLT/2qr9uDAGEYehCaKBM/jRYVuazphvJ2UKFSi3iL9mixG aQ0GCOa4sYX4TNeH8183+IPH5ZMsuipk4JLoIma7HENhVzB8NChysY6KwwD1831uNtM/ +3WXdRhoaqVpJjK79IJTtDdk6xzZu/bUyGGJiIDTGqd/WzyHGW1F1cmVfoFhJSY782zB uiYHMKE5M1+QSJcTooPXbsfikIYv+SpW+lvY6r+wB4pd7aB1fkq5+Wp2emSrNGJKP6uM yJsRvP1npOSQcw0Dfg4wgs560DKnyXRN61abPP0RfC798LoEAOUNKXY8Gxq08B6Bzuzw aYaA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=L9A2I5qq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::530 as permitted sender) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+C/tfX7vT1mOdP4O80ejBhV08ZLnkT4XkjEN3CMWzbI=; b=iDgtLoHsPNOGqVpEg+y/O+8EdrJG8kNn/YW6z8nmLd8hCfHEoSPr8J9F7t8IKtW5mM sdDTLK60Z4Y3hMjwhD+mfYj9mgHBgmoASeYNlvNI8DV0d8jrYWl/j5C7PdGlbyhraf5s H1je7g3UUGvZmk2reMG0+ExUd0VTD+wZyWWZbC717lgwzF5fsjAISTdBhy6EHZmMlv0I E4Lu3FIsUjjHmAg5OuxjLecNnU2ZmwMgDtIgdtX4RMggTFjT2TAzI+fzjHqWH9QY3zZx KdlFNcPFpUJqL53BTGyPSrzORVq5xI4pBD8gufqOLZ/eMiPwMM30ZOqWc0vf//D76Kkf ylZA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:mime-version:from:date:message-id:subject :to:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=+C/tfX7vT1mOdP4O80ejBhV08ZLnkT4XkjEN3CMWzbI=; b=g2f+8YzO/hKRFu80foDMokTcdqSSN3zFo9KJdb16KVRS9qwQqrie8HLfdJWAaq5pcI jSkJnYQGyvKI1XgVu5xfrvXWMqQ2NTx9LRc3qinrA6GDr4cvwTyLtQn8fuzvG/J9ASJC KAtmjBALdGwo+t1Gk5ojjYDSM4EmFtQybEa3A9yageI92qF897c9K7jeJW4B2dhBDxOx /80iTWcE4YLqsdpEOAky9cABApHKybnANYIRRJLrEngljI2QAZjez7B2HHTcJTOBVqJm fa2qhBRY/cppcYFn1ZKjS9lypyl0a6lklb2hbHlW74hgiy+HLu+ycEngt71HR8tlI4Q4 66SQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUvj71+JnNJ6gA4YsB1NXASQajqA5MNEoKnuLAIUG0KgrMKCQxa 0dEglFe+AYGI28JeTZofBf4= X-Google-Smtp-Source: APXvYqzjSaZCjIHMrAlkHO4YFghFDF1TtvkYhw7iADOz7Wn0BUT1D4HspuwI6JTr1fb8bjCRKuaG1w== X-Received: by 2002:a2e:884d:: with SMTP id z13mr2556796ljj.62.1568821370014; Wed, 18 Sep 2019 08:42:50 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac2:4190:: with SMTP id z16ls8804lfh.7.gmail; Wed, 18 Sep 2019 08:42:48 -0700 (PDT) X-Received: by 2002:a05:6512:75:: with SMTP id i21mr2442089lfo.95.1568821368409; Wed, 18 Sep 2019 08:42:48 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568821368; cv=none; d=google.com; s=arc-20160816; b=YZDPB/skLDV0CyEIVJmZQpIMG/F7f1Q738vSVj3w4WC+ta1lj2U9RWKRSOqUqWHfUf HZegFA3bFA5cWDHDhsEojdFRGAxiuIpMS2+i7QommoNgFBvMF/JuN8xN4Yku0/Godb+4 Z76aBvFcnLe0rQQtj31lOvO/s01pCnXTu/7M14KnSmtjUqsPNvtKYe8Nz4jnN8mr8sDi SKDyrEfAXN+Azyi8pQuqaTccNJKXAiUwYjI1iscpIorQWanjOMCG63JcrKHP1cBVVpi5 No9ubfR7x2syV+zcwZdgktxaWYZ9MT+FkxGO+gYk1Y7R7fpQd/ULyWXssGlrLoOBQRbY 6XEQ== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature; bh=I6J7WX83XUWgzB5RvM6QcUH9zGl8yhvtpCBkl0ui1tk=; b=C5ZIhdmPEXS/8vsmuK04NTRyQB9LiXh3yThTP11EenNxrNHTLPIH9l7NNp4JFQWVxg Ai3CxGIlwJHOq/AxzvlIfSAxLn3NCBqyQ0oyrO20RbhGLexkmIfwpONnn4Ew2UGawOTf B9oEfjD1iHqBnk8yuYkU2yrUY5hPYWZ9aNrsmu2Rhdy88XwplzziqpTQ46bEudcvMuzE 4t7ZtO1MCLDQSKYywCkAGJ1wQokUmwTYBv8579rnOBxCW4k2/xfg+VrLrHWqTE0hnuNe Qw11oW/L1NR/fC8wKGhEdtzqfy4cV1oDbNLq2F25imw/Qv/WBuvyBls7cPa4yMRGhsfE k2pQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=L9A2I5qq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::530 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-ed1-x530.google.com (mail-ed1-x530.google.com. [2a00:1450:4864:20::530]) by gmr-mx.google.com with ESMTPS id h2si182933lja.2.2019.09.18.08.42.48 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 18 Sep 2019 08:42:48 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::530 as permitted sender) client-ip=2a00:1450:4864:20::530; Received: by mail-ed1-x530.google.com with SMTP id r9so390897edl.10 for ; Wed, 18 Sep 2019 08:42:48 -0700 (PDT) X-Received: by 2002:a17:906:7fda:: with SMTP id r26mr2503953ejs.170.1568821367594; Wed, 18 Sep 2019 08:42:47 -0700 (PDT) Received: from mail-wr1-f46.google.com (mail-wr1-f46.google.com. [209.85.221.46]) by smtp.gmail.com with ESMTPSA id j5sm1102858edj.62.2019.09.18.08.42.46 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 18 Sep 2019 08:42:46 -0700 (PDT) Received: by mail-wr1-f46.google.com with SMTP id r3so7447194wrj.6 for ; Wed, 18 Sep 2019 08:42:46 -0700 (PDT) X-Received: by 2002:a5d:430f:: with SMTP id h15mr3624192wrq.177.1568821366261; Wed, 18 Sep 2019 08:42:46 -0700 (PDT) MIME-Version: 1.0 From: Michael Shulman Date: Wed, 18 Sep 2019 08:42:33 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: [HoTT] Recovering an equivalence from univalence in cubical type theory To: "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=L9A2I5qq; spf=pass (google.com: domain of shulman@sandiego.edu designates 2a00:1450:4864:20::530 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Precedence: list Mailing-list: list HomotopyTypeTheory@googlegroups.com; contact HomotopyTypeTheory+owners@googlegroups.com List-ID: X-Google-Group-Id: 1041266174716 List-Post: , List-Help: , List-Archive: , Let Equiv(A,B) denote the type of half-adjoint equivalences, so that an e:Equiv(A,B) consists of five data: a function A -> B, a function B -> A, two homotopies, and a coherence 2-path. Using univalence, we can make e into an identification ua(e) : A=B, and then back into an equivalence coe(ua(e)) : Equiv(A,B), which is typally equal to e. Now we might wonder whether coe(ua(e)) might be in fact *judgmentally* equal to e; or at least whether this might be true of some, if not all, of its five components. In Book HoTT this is clearly not the case, since univalence is posited as an axiom about which we know nothing else. But what about cubical type theories? Can any of the components of an equivalence e be recovered, up to judgmental equality, from coe(ua(e))? (My guess would be that at least the function A -> B, and probably also the function B -> A, can be recovered, but perhaps not more.) -- 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 HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/CAOvivQzzSXNHs%2BzbPQTyHEuU53aHXJ0sPe4pr%2Byf0ahLGvUpVA%40mail.gmail.com.