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=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_EF,HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qt1-x83a.google.com (mail-qt1-x83a.google.com [IPv6:2607:f8b0:4864:20::83a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 02a6614d for ; Tue, 11 Jun 2019 17:02:41 +0000 (UTC) Received: by mail-qt1-x83a.google.com with SMTP id z6sf5154999qtj.7 for ; Tue, 11 Jun 2019 10:02:41 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1560272561; cv=pass; d=google.com; s=arc-20160816; b=JXdG6yddJygGp6T91Q1MSf8C7lrjHp6m4FebAnJuVywvlS7UvAEshHnVXiPf4uNLzc XoU0YLUoxJmOcM46F8LPYNe8yld1k95cPi2jlS232Z65/HeetkGWC9M5G3sM/aIW5tyN Jg/0G9w/DCwmsYQpPkbhqQiAj9yN928lI9nIeZUaKDGM0yv07zkpssBlKzOmHUACubm3 xKA8bKLkzaxPxOR436iqC39brTm/Y0CTgVj4N2/vSyYjnFGkEwdiOpkHX3Geq3epacKs Th2VS19mcd8LOgE8C2ZkhmusPjQMohiP/jE9szq2YQjjom9OaVjyxEgDyYCVP6FNX0YY sgdg== 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=9bZIEgPyGOJJOibCiP6ThIxZn80B/dagY5h0areyXAI=; b=MJFaPW/gpRD4PFDkQ2ImECGIrqqiIPJlT8FYrTk/2A9nGoivV/JIPdxdouUHBYzSOU uZTTKinTkffWCu/iAWRZV2y6jqmZUPAkECIzWpnDrgeY2IoGEDOCzpT7EegZbeu8DUVQ zAoyyOfVTftldTiYtACzYNXMVNaI4mjlmYivr82SkynSidcoOa/lYFgpSJUI0TH0yZyy bhv06oW1XbfLyjhAang2CtwzRD/4+5ItiLjC22UmKGjOclCFYR/Mb/jymycPKOHj7z1s DtjL8DMlSa+DkPiClV+zo97Lb+2Sb/uUWwf54PfLcljKgpCC5FutoqiB4przhIOTG8aO ZS7A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WxTE5v+o; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c41 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=9bZIEgPyGOJJOibCiP6ThIxZn80B/dagY5h0areyXAI=; b=ChwEJ5cRYCFmQ1hrAtkgb4N7dMQ42pq6aWG0vs2XJjxjVaKxVbBAStsRJQ/EokkIsk BkA+no+ObiafnmuFQt4bBvEqm/DhYzPNRvcrhGrAVcdH2FfJBmPtdHThvVLfZ3zgdUzO ILT6t4tQXNuoHAGOzKhPuguMqX6G/EP0so9NUhNaSOwC1K9zxUO9g7gJsg3zwBLZFUxH yQ58vUlLAFliiksAgCmAjxkK+x4xBiCnxubb34NQdAIueldRiH6LzzYzRaxaGRDSD5zc 5LYhjr+cg/jNeRX23f4VC3h15qOveZaAQw7WFR/O/1SAa3waZzsxKGuwBouAdByQVB0i yV0g== 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=9bZIEgPyGOJJOibCiP6ThIxZn80B/dagY5h0areyXAI=; b=gOViDNCc4XFsPLNMilcdvy+Ra8iZ4ObEvTlzWdl4MInXx5SbPe3Ief/VimVq53qCnr MD6wxouATXbmJReTZK19S7sPwiW21x0Whjdxi4k+4/B3O/cfNnRG3EaZ/M5Icz2/u01/ cT/FU3QAAxvn+TmF3z0C/zIVw7CjYX3sOK+llVLVlHpbmRiElEGRX4N61UJpkUiSmkds BRBUxY1IimCFHSG7wvbpArGW5cxHElDDjkqFGEmztFBNqQ2K0EAX/3tQ6AHcvc+G+VyW vDodXkGKtZyfrwmJLHTTKriAMXUoO4XcrexzfDih7gRc2BWmDY6Y2o/EhHEC1Ut5B//V o2bA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAWob/F3d0ogm+VdBM0LtdolUugbTINXy+7eQo5sBREb+ve807Y7 cuGum1wB05y2qsuxjBpJ5R4= X-Google-Smtp-Source: APXvYqyAKH2LHnsw6h2nx3vrVY84OH5Zi/71l4zTJFzTAsup5VJzo0+7D9u9MsMWggwZwqbdG44F4Q== X-Received: by 2002:ac8:2b62:: with SMTP id 31mr66073796qtv.140.1560272560470; Tue, 11 Jun 2019 10:02:40 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:4f85:: with SMTP id d127ls1549198qkb.4.gmail; Tue, 11 Jun 2019 10:02:40 -0700 (PDT) X-Received: by 2002:a37:6a87:: with SMTP id f129mr46508574qkc.183.1560272560146; Tue, 11 Jun 2019 10:02:40 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1560272560; cv=none; d=google.com; s=arc-20160816; b=OGBsUwuY18yhK60gZkunztilvfOZAs1H29xwdlv0qBFcCBrmr6f/BU/J0erRR2mzJp kWQvhU44XMZyOlVF5iCsUQP7kv+x8nFtpua3fQm2p/EPx/MkxfKPQb8V1GE6xf54PeQ+ 431R9RqcwAyev5MLXFZtFEuj0TKHYSKvofGVjNH0Y72arbSYjCEQv6hfFZFnfHqbp1+i eN1AoS/xR3ZRnghQzbAcmYgazeTbb13ydeS6ZNR+QhYmR/Mh/fgRhkOBnZdEGUO6xZWB pF7DNZzoc5u3jPze7v1Fa2y2EvkrWGTfQLC9MSh8IwckBt3NR0Vn+Z0FqLwQn/+/077Z lb4g== 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=9yohOqynhlUaAXFS/WLza9M2NLPDBQW4DQ9D+fn3hj0=; b=UhRquI0sibLz98dFt5EvVr/4RCUDkXS1zzxFIZ7xOvG+2SK4/MDiT9QvxPnJqGHOpf pMG7Er8ZblCKBIn+eTfn8d1JF6ppcNd7TB3b/ccNuvxnrols1TWT/UU+5/AyjQgKkwmq RrcxkoYc43jE5ul0tlpnKRdtMljXRdCJdH1ZJzx/gEMyibTma02bB7UL3sSNT6hqcxK+ DYJQ4XbuXbGQ5uCY00sjnQZDlqrDxJiiRAxTjwQuBlNKAY1Ca0l9BTT1umSAmAyRG6ik cFKzIm+F1w7Istat1dU/1DP/1g+idZT3UfikCj0FD5OUsSVYA0J00dw4ZvcEKGYP1+IZ HuuQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=WxTE5v+o; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c41 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc41.google.com (mail-yw1-xc41.google.com. [2607:f8b0:4864:20::c41]) by gmr-mx.google.com with ESMTPS id c39si416437qta.5.2019.06.11.10.02.39 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Tue, 11 Jun 2019 10:02:39 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c41 as permitted sender) client-ip=2607:f8b0:4864:20::c41; Received: by mail-yw1-xc41.google.com with SMTP id k8so5590186ywh.0 for ; Tue, 11 Jun 2019 10:02:39 -0700 (PDT) X-Received: by 2002:a81:aa50:: with SMTP id z16mr20078732ywk.278.1560272559575; Tue, 11 Jun 2019 10:02:39 -0700 (PDT) Received: from mail-yb1-f177.google.com (mail-yb1-f177.google.com. [209.85.219.177]) by smtp.gmail.com with ESMTPSA id a187sm4267685ywh.21.2019.06.11.10.02.39 for (version=TLS1_3 cipher=AEAD-AES128-GCM-SHA256 bits=128/128); Tue, 11 Jun 2019 10:02:39 -0700 (PDT) Received: by mail-yb1-f177.google.com with SMTP id c5so5384101ybk.6 for ; Tue, 11 Jun 2019 10:02:39 -0700 (PDT) X-Received: by 2002:a25:d08:: with SMTP id 8mr35644831ybn.395.1560272558773; Tue, 11 Jun 2019 10:02:38 -0700 (PDT) MIME-Version: 1.0 From: Michael Shulman Date: Tue, 11 Jun 2019 10:02:27 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: [HoTT] Are cubical sets hypercomplete? 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=WxTE5v+o; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c41 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: , I have always assumed that cubical set models, like the simplicial set model, satisfy Whitehead's principle (one form of which is the statement that if all n-truncations of a type are contractible, then it is contractible). However, since cubical set models aren't known to have an underlying model structure that's equivalent to simplicial sets (and, as discussed previously on this list, at least one model structure for cubical sets is known to be *not* equivalent to simplicial sets), it's not completely obvious to me how to prove this. Has anyone checked carefully that one or more cubical set models satisfy Whitehead's principle -- and in particular, is the argument fully constructive? I could imagine that it might require something like countable choice. -- 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/CAOvivQyPJsVzRtJw7uWX%3DLJH0-3r7TarVm%3DCSaqfoFU4k7foqw%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.