From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDSLFPUN3EPBBFMPUTNAKGQERBZXTSQ@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-io0-x23e.google.com (mail-io0-x23e.google.com [IPv6:2607:f8b0:4001:c06::23e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2eab994d for ; Fri, 13 Jul 2018 20:12:07 +0000 (UTC) Received: by mail-io0-x23e.google.com with SMTP id s14-v6sf11554680ioc.0 for ; Fri, 13 Jul 2018 13:12:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531512725; cv=pass; d=google.com; s=arc-20160816; b=Z5wbpMuzbwwdnDhvgvSRI/VABCK0+vYad0KscsKpBBhlMK4LtmKJIyWkqUmoG852TS Rtw9hnNxCoEsJ4ChLAimwsJw6u94KtU1/JZeaZaWdx7lCjK2HE6VXigEUvxtBrDnWG2m h4tyz4GgrmlqKXsr/L39N7DvFtpNY6OLoYjgBEagwACewkF8cnU4v2pCfH9/gEq6rq1S X88ntUrHswYjnYaojF8wRbw61i9//6Lm3H2oEt5V29pWFy9GsPcxrC4/Fj4oLdPzqsCx rWca1BOK7DC/CYV6DaDDZeFUxzvV7otZCaDcmNO3/xOlHZ5pBY7obnGJRtuEMPc5nJVp 5yZg== 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:arc-authentication-results:arc-message-signature :sender:dkim-signature:dkim-signature:arc-authentication-results; bh=nFxr8s+s0t5An9ueLJCCYoHgcifYHk9kwvMeo4X2VjQ=; b=rImggoSVL9aQezOfPCNTL565sP6UDCuPIcUg0Nm3uaLTmo70iwN8jMHePltQvQI1q1 u7BVmn3kpmPT7zCRXs7ZhkA9MAlsnO6qtFjc9ICIGald+toybjKVghPo7WscgHkM0/PB 9d8VN+KlNYjbxW123u5JoAa6zIZRdcgAg6JVLAOEjYi5XOztxk+NnQf4l6ZT8Is3Sjit UQj1gpvQtXw7Yhx6mDBiD4LJRSfTE2Vqn/GXWYx1El8LL9uC5Kqd9uZqALTj82iSJCm8 El1JmZERV0Wg8ysVaklWaR43QZ4FizfX/rbNt9B6hkD8VQ7JR4LOpTjcUf+c4aBHfmir F/9g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=fGk+cY2A; spf=pass (google.com: domain of sattler.christian@gmail.com designates 2607:f8b0:4864:20::530 as permitted sender) smtp.mailfrom=sattler.christian@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=nFxr8s+s0t5An9ueLJCCYoHgcifYHk9kwvMeo4X2VjQ=; b=LJAFRb7vNv4xEXQPYHZhLDz2bZ4J/l0xmQKGwV3IXQJcFziOAclJEPBhYnsBaocpTV FyPWtHNvtNl8hpxRd5gOBWpyfD49fSHIiXwpGqP/alYS/N4goa6c9D9MBk9mK9YGNdIv RpVP3cCH3ULgBtcB6jRTna5WtF3SWiIrPsYh/lVgNchPYrsuOVONquNTeMrKZ0cRa/J2 2JzlEpg0eEwafCl9E3JfjSHY1HgYDliC0GWIu4Zhs2X3oq7WQvgaDUouqkllc2nlI33i GlyEdGxL/VatgTvXz9A4Ztg5iLMKkWVj8p7j8PbZLZ57KsMWCt+OxY7WpNIZydQfvJMi Nrpg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=nFxr8s+s0t5An9ueLJCCYoHgcifYHk9kwvMeo4X2VjQ=; b=g3Kukm13/HwYflocqEmahamVd5dvQmRJln1IEQ5qNPDdtKNMMk5FIqlZ8DMqvEieZh glF+EBUEsY5+H3Q1M/kJkmZXfQrhUSmChUbzKXob/pJKvoUGEoWq8Q5TtGXsrk91Kk1R lWpdCN6mLeKqZParlKe4pXfqg0Lr3wT4aOa/DHe+eDghknrY3Vlsqb/Ur0dNaECbtCzy bIlCmAPIWQ8OjpO/7eRTkubRLxzyPeFeApmr6eKodwnsIsmCUZ+XBqGcDBpHrOaKvGrJ dkEFVWB86wgo46+vgLCAVNb2Iq9kJ6DR+IhrfZ357D+XbwbNxCk04bMNB0x9M1W9KHw9 xXgg== 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=nFxr8s+s0t5An9ueLJCCYoHgcifYHk9kwvMeo4X2VjQ=; b=NKSxS/oM7HeLy7M/fWq1S/z7fgbQuLm9BQHSbI3bZ7JueCUBqLwXKp3Jxo27zwHeap Uj14JLswsA+tlw/9JG+iXbtGHFlkjLRkXdbZOiss2qUGStEbwgK8EzM19Z4istvl91/j 2edzEBoS8KzXWxTGifpEX6s6V6BECjXLBU5kKCd5Hf0gXoisw1fNFNJtbZBTJrMUDEZK Vm2Wb4AlBQ4YV5jolCFWzKFLH31OlMhnzSnXrK5k+zZg3qCbvO3T6lOGEi9VuKJ4pLjV e6UcmZt3+0OfBDGJeTxK9yl7hOdnQpTUZ04kDycEHSDzQZGlBEwBajlHVdy8Ki1OaIWs zdvw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGotVz/qiH0Aulkz3TGCDsjLdb+Li7+VegKLSCLJfR0KpPp334U ocYLS1mP0ReQR+vkfho4Yak= X-Google-Smtp-Source: AAOMgpdu9FrV0SEOxXDP72oxiwMLycW7FfcYm7GJn/cdLEQ1/e82ASMNKOcG05uXCBAwATUochiFNQ== X-Received: by 2002:a5e:d70d:: with SMTP id v13-v6mr28503iom.6.1531512725654; Fri, 13 Jul 2018 13:12:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a02:7349:: with SMTP id a9-v6ls3924802jae.3.gmail; Fri, 13 Jul 2018 13:12:05 -0700 (PDT) X-Received: by 2002:a02:4d:: with SMTP id 74-v6mr3402377jaa.15.1531512725290; Fri, 13 Jul 2018 13:12:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531512725; cv=none; d=google.com; s=arc-20160816; b=kpW6DT+bcnx9tgndLimqkdt7ES/DtpgKwSETh08Ne7TSyCiAcSmK2xlJKDcyYmsidm y260N/LmpV5V03CfD26y3PbY/08JH+d6GsCEDPTUHL+6W4/Gbv9lA07/qxQA5oaPN19I timwMg/+M7y+Xvu9z4AI/kGgglhktrHQDImZmW5Nm7+oYvcMYS/u86kAAOPrsaZWQzwm 525qJfm+3bqm1gPWRp+B5Gz9YwnFMFP5F4ohgDb1q8aqLf2l4p54pHnjswiAAGRjxGh0 irXstmZsc/01y0+13WMNvluf+ZfCnSdY/WsN8klogg4JmLhsZSp4ZEYLfhG85tXoKGqu rJ8Q== 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 :arc-authentication-results; bh=UeU5HzLf6hKmklbGVuBDwRysLtdNy9tIhwg9NjgMhl8=; b=MrPH0I35eR/Q703zF3wjYOtFlR0s4x0snnVf0LdJnHg6iB0BZE/Dr0ffeyXx8ZrtfW 4jvGJ5nR+GhfdLVd5yG/Ks6RQM3ca8EmwNk4vEmRn166S+UiPivbhAvxWC3BUK0jpfiK meCIeWl7kKsCpZDQ514ikgY3V2WgTOL7hniWWi3Cc8ovZ9nbYPvOxTQU3p57xEE9l4nP iSWW0lt3XHA33GIeCC5CXuEPJKvaLbMKj/p0YSYGIpWwM7LTowYIvs0ZIYs0wyNT/Yw5 Cr6R5pcQo5W1UmIWzUMXPgaehCOIj5y+Sfc5BgrfzOdSuCzA/TgS026rylwXSAhLecSt BK7w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=fGk+cY2A; spf=pass (google.com: domain of sattler.christian@gmail.com designates 2607:f8b0:4864:20::530 as permitted sender) smtp.mailfrom=sattler.christian@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-pg1-x530.google.com (mail-pg1-x530.google.com. [2607:f8b0:4864:20::530]) by gmr-mx.google.com with ESMTPS id g132-v6si292779itd.2.2018.07.13.13.12.05 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 13 Jul 2018 13:12:05 -0700 (PDT) Received-SPF: pass (google.com: domain of sattler.christian@gmail.com designates 2607:f8b0:4864:20::530 as permitted sender) client-ip=2607:f8b0:4864:20::530; Received: by mail-pg1-x530.google.com with SMTP id n9-v6so5030266pgp.12 for ; Fri, 13 Jul 2018 13:12:05 -0700 (PDT) X-Received: by 2002:aa7:87d0:: with SMTP id i16-v6mr8524927pfo.82.1531512724416; Fri, 13 Jul 2018 13:12:04 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a17:90a:30c2:0:0:0:0 with HTTP; Fri, 13 Jul 2018 13:12:03 -0700 (PDT) From: Christian Sattler Date: Fri, 13 Jul 2018 22:12:03 +0200 Message-ID: Subject: [HoTT] homotopy groups in CCHM cubical type theory To: homotopytypetheory Content-Type: multipart/alternative; boundary="000000000000e86c3b0570e717a8" X-Original-Sender: sattler.christian@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=fGk+cY2A; spf=pass (google.com: domain of sattler.christian@gmail.com designates 2607:f8b0:4864:20::530 as permitted sender) smtp.mailfrom=sattler.christian@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --000000000000e86c3b0570e717a8 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable When computing homotopy groups of spheres in a version of cubical type theory, one might wonder whether this says anything about the corresponding homotopy groups of spheres in standard homotopy types; a priori, it might happen that we get different homotopy groups. Thierry Coquand has answered this question positively for CCHM [1] cubical type theory without reversals (from here on simply referred to as CCHM): given numbers n, k, a=E2=82=81, = =E2=80=A6, a=E2=82=9C, if we can derive =E2=8A=A2 =CF=80=E2=82=96(S=E2=81=BF) =E2=89=83 =E2=84=A4/= (a=E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C) in CCHM, then w= e also have a corresponding external isomorphism =CF=80=E2=82=96(S=E2=81=BF) =E2=89=83 = =E2=84=A4/(a=E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C) for t= he standard k-th homotopy group of the n-sphere. This email serves to document his argument. Let =E2=96=A1 denote the full subcategory of posets on objects [1]=E1=B4=B5= for I a finite set (=E2=96=A1 can also be described as the opposite of the Lawvere theory = for distributive lattices). We wite cSet for the category of cubical sets, presheaves over =E2=96=A1. The presheaf represented by [1]=E1=B4=B5 will be= written =E2=96=A1=E1=B4=B5. Cubical sets form a model category where the cofibrations are the levelwise decidable monomorphisms and the fibrations are the maps admitting a uniform Kan filling operation in the sense of CCHM. We have a combinatorial description of homotopy groups =CF=80=E2=82=96(X, x=E2=82=80) (as definable= in any model category) of pointed fibrant objects (X, x=E2=82=80) in cSet: the underlyin= g set is the quotient of maps =E2=96=A1=E1=B5=8F =E2=86=92 X that are constantly x= =E2=82=80 on the boundary =E2=88=82=E2=96=A1=E1=B5=8F by homotopy (relative to the boundary); the group structure is given by degeneracy and suitable Kan composition of cubes. Recall that CCHM has a model in cubical sets. We write =E2=9F=A6-=E2=9F=A7 = for the interpretation of types and terms and interpret types in the empty context as fibrant cubical sets. Given a pointed type (X, x=E2=82=80) in the empty = context, we can verify that the points of =E2=9F=A6=CF=80=E2=82=96(X, x=E2=82=80)=E2= =9F=A7 are in bijection with =CF=80=E2=82=96(=E2=9F=A6X=E2=9F=A7, =E2=9F=A6x=E2=82=80=E2=9F=A7). A bit more (straightforward, though tedious)= verification shows that the group operations of =CF=80=E2=82=96(X, x=E2=82=80) defined internally i= n CCHM have as interpretations maps of presheaves whose actions on points correspond to the group operations of =CF=80=E2=82=96(=E2=9F=A6X=E2=9F=A7, =E2=9F=A6x=E2= =82=80=E2=9F=A7). We can define =E2=84=A4/(a=E2=82=81) =C3=97 =E2=80=A6 =C3= =97 =E2=84=A4/(a=E2=82=9C) in CCHM so that the interpretation of the type of group elements and the group operations is (up to isomorphism) constantly at every level the group =E2=84=A4/(a=E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C). Reca= ll that S=E2=81=BF in CCHM is defined as a higher inductive type generated by a base point b and an n-cube whose boundary is constantly b. This is interpreted as a fibrant replacement 1 +_{=E2=88=82= =E2=96=A1=E2=81=BF} =E2=96=A1=E2=81=BF =E2=86=92 =E2=9F=A6S=E2=81=BF=E2=9F=A7 in cSet. Interpreting the derivation of =E2=8A= =A2 =CF=80=E2=82=96(S=E2=81=BF) =E2=89=83 =E2=84=A4/(a=E2=82=81) =C3=97 =E2= =80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C) in cubical sets, we obtain an external group isomorphism =CF=80=E2=82=96(= =E2=9F=A6S=E2=81=BF=E2=9F=A7, =E2=9F=A6b=E2=9F=A7) =E2=89=83 =E2=84=A4/(a=E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C). The type theoretic part of the argument is now finished. The rest of the argument relates homotopical aspects of cubical and simplicial sets. Let us briefly recall the relationship between these two settings. We assume classical logic from here on. Let =CE=94 denote the simplex category, the full subcategory of posets on objects [n] for n =E2=89=A5 0. We write sSet for the category of simplicial= sets, presheaves over =CE=94. The presheaf represented by [n] will be written =CE= =94=E2=81=BF. Recall the Kan model structure on sSet; it is the standard model for homotopy types. The cofibrations are the monomorphisms and the fibrations are Kan fibrations. Recall from Kapulkin and Voevodsky [2] that simplicial sets may be seen as a Grothendieck subtopos of cubical sets. We write C : sSet =E2=86=92 cSet f= or this fully faithful functor; it can be defined as CA([1]=E1=B4=B5) =3D sSet((=CE= =94=C2=B9)=E1=B4=B5, A). Its left adjoint S : cSet =E2=86=92 sSet is the triangulation functor, the coco= ntinuous extension of =E2=96=A1 =E2=86=92 sSet sending [1]=E1=B4=B5 to (=CE=94=C2=B9= )=E1=B4=B5. We will also need that S has a further left adjoint L : sSet =E2=86=92 cSet (see [2]), the cocontinuous ex= tension of =CE=94 =E2=86=92 cSet sending the poset [n] to its cubical nerve, the cu= bical set that at level [1]=E1=B4=B5 is Poset([1]=E1=B4=B5, [n]) (note that L and C a= gree on representables). This gives an adjoint triple L =E2=8A=A3 S =E2=8A=A3 C wit= h L and C fully faithful. We include at the end of this text a few useful facts about the interaction of the functors L, S, C with the model structures on sSet and cSet that will be quoted in the following. Continuing with the main argument, recall that 1 +_{=E2=88=82=E2=96=A1=E2= =81=BF} =E2=96=A1=E2=81=BF =E2=86=92 =E2=9F=A6S=E2=81=BF=E2=9F=A7 is a fibrant replacement in cSet. By (3.), S is both a left and a right Quillen functor, so we have that S(1 +_{=E2=88=82=E2=96=A1=E2=81=BF} =E2=96=A1=E2= =81=BF) =E2=86=92 S(=E2=9F=A6S=E2=81=BF=E2=9F=A7) is also a fibrant replacement in sSet. Note that S(1 +_{=E2=88=82=E2=96=A1=E2=81=BF} =E2=96= =A1=E2=81=BF) =E2=89=83 1 +_{S(=E2=88=82=E2=96=A1=E2=81=BF)} S(=E2=96=A1=E2= =81=BF) (weakly equivalent to 1 +_{=E2=88=82=CE=94=E2=81=BF} =CE=94=E2=81=BF) presents the = n-sphere in simplicial sets. So S(=E2=9F=A6S=E2=81=BF=E2=9F=A7) really is a fibrant model for the n-sphere = in simplicial sets. Note that we have the same combinatorial description of homotopy groups for fibrant pointed objects (X, x=E2=82=80) in simplicial sets as we did in cub= ical sets, with the underlying set of =CF=80=E2=82=96(X, x=E2=82=80) given by th= e quotient of maps (=CE=94=C2=B9)=E1=B5=8F =E2=86=92 X that are constantly x=E2=82=80 on its b= oundary by homotopy and the group structure defined using degeneracy and the same Kan composition as for cubical sets. It remains to construct a group isomorphism =CF=80=E2=82=96(=E2=9F=A6S=E2= =81=BF=E2=9F=A7, =E2=9F=A6b=E2=9F=A7) =E2=89=83 =CF=80=E2=82=96(S(=E2=9F=A6= S=E2=81=BF=E2=9F=A7), S(=E2=9F=A6b=E2=9F=A7)). We have a canonical function =CF=80=E2=82=96(=E2= =9F=A6S=E2=81=BF=E2=9F=A7, =E2=9F=A6b=E2=9F=A7) =E2=86=92 =CF=80=E2=82=96(S= (=E2=9F=A6S=E2=81=BF=E2=9F=A7), S(=E2=9F=A6b=E2=9F=A7)) given by the action of S on morphisms. This is a group homomorphism since S takes the combinatorial description of the homotopy groups in cubical sets to the one in simplicial sets. We are left to show that the function is a bijection. Surjectivity is given by (5.) with f' the constant map on =E2=9F= =A6b=E2=9F=A7. For injectivity, consider maps u, v : =E2=96=A1=E1=B5=8F =E2=86=92 =E2=9F= =A6S=E2=81=BF=E2=9F=A7 constantly =E2=9F=A6b=E2=9F=A7 on their boundary such that S(u) and S(v) are related by a homotopy H : =CE=94=C2=B9= =C3=97 S=E2=96=A1=E1=B5=8F =E2=86=92 S(=E2=9F=A6S=E2=81=BF=E2=9F=A7) that is constantly S(=E2=9F=A6b=E2=9F=A7) o= n S(=E2=88=82=E2=96=A1=E1=B5=8F). A lift of H to a homotopy between u and v (relative to their boundary) is then given by (5.) with f' given by u and v on two opposing sides and constantly =E2=9F=A6b=E2=9F=A7 e= lsewhere and g given by H. Remarks: - Recall that there is more structure in a standard homotopy type than just its list of homotopy groups. It seems the above argument also applies to operations involving multiple groups simultaneously, for example the action of =CF=80=E2=82=81 on =CF=80=E2=82=99, as long as we can combinatorially de= scribe these operations using cubical filling in the same manner in both cubical and simplicial sets. - The argument generalized from spheres to other finite cubical cell complexes. Appendix. (1.) L preserves cofibrations and weak equivalences. Using cocontinuity of L, one sees that L(=E2=88=82=CE=94=E2=81=BF) is the s= ubobject of L(=CE=94=E2=81=BF) that at level [1]=E1=B4=B5 contains the non-surjective poset maps [1]=E1=B4= =B5 =E2=86=92 [n]. By cocontinuity, since L sends boundary inclusions to cofibrations, it preserves cofibrations. For preservation of weak equivalences, by Ken Brown's lemma and cocontinuity, it will suffice to show that L sends horn inclusions to weak equivalences. Using cocontinuity and 2-out-of-3, this can be further reduced in the standard way to showing that L sends representables to weakly contractible objects. Recall that L[n] is the cubical nerve of the poset [n]. Note that [n] has an initial object, hence is homotopy equivalent to 1. Applying the cubical nerve, we get a homotopy equivalence between L[n] and 1. (2.) S preserves cofibrations and weak equivalences. As a right adjoint, S preserves monomorphisms (i.e. cofibrations). It also preserves products and pushouts and sends the interval in sSet to the interval in cSet. Thus, it sends prism-style generating trivial cofibrations in sSet to trivial cofibrations in cSet. By cocontinuity, it preserves all trivial cofibrations. By Ken Brown's lemma, it preserves weak equivalences. So we obtain: (3.) both adjunctions L =E2=8A=A3 S =E2=8A=A3 C are Quillen adjunctions. In particular, S preserves all three classes of the model structure. (4.) The pushout application (Leibniz application) of the counit =CE=B5 : L= S =E2=86=92 Id to the boundary inclusion =E2=88=82=E2=96=A1=E1=B4=B5 =E2=86=92 =E2=96= =A1=E1=B4=B5 is a weak equivalence. We generalize the claim to any face lattice subobject M =E2=86=92 =E2=96=A1= =E1=B4=B5. Using cocontinuity of LS and closure properties of weak equivalences and trivial cofibrations, if the claim holds for two such subobjects M=E2=82=81 and M= =E2=82=82 as well as their intersection, then also for their union. Thus, it remains to prove the claim for face map inclusions =E2=96=A1=E1=B4=B6 =E2=86=92 =E2=96=A1=E1= =B4=B5 and the empty subobject 0 =E2=86=92 =E2=96=A1=E1=B4=B5. Using cocontinuity and closure properties once more, this reduces to the claim just for 0 =E2=86=92 =E2=96=A1=E1=B4=B5. So we need to prove that =CE= =B5_{=E2=96=A1=E1=B4=B7} : LS=E2=96=A1=E1=B5=8F =E2=86=92 =E2=96=A1=E1=B5= =8F is a weak equivalence, i.e. that LS=E2=96=A1=E1=B4=B7 is weakly contractible. Th= is can be seen via an explicit contracting homotopy based on the initial vertex. Alternatively, we may proceed as before and generalize the claim to LN where N is a union of injections =CE=94=E1=B5=90 =E2=86=92 (=CE=94=C2=B9)= =E1=B4=B7 that preserve the initial and terminal vertex. Using cocontinuity of L and closure properties of weak equivalences and trivial cofibrations, the claim reduces to the case of L=CE=94=E1=B5=90, which we already know from (1.). Note that the lack of a Reedy category structure on =E2=96=A1 prevents us f= rom using the preceding statement to show that =CE=B5 is generally valued in we= ak equivalences. Note also that those cubical sets local (in the 1-categorical sense) with respect to =CE=B5_{=E2=96=A1=E1=B4=B5} for all I are exactly the sheaves of= Kapulkin and Voevodsky [2], i.e. the cubical sets coming from a simplicial set under application of C. (5.) Let X =E2=88=88 cSet be fibrant; given f' : =E2=88=82=E2=96=A1=E1=B4= =B5 =E2=86=92 X and g : (=CE=94=C2=B9)=E1=B4=B5 =E2=86=92 SX such that S(f') is g restricted to its boundary, there is f : =E2=96=A1=E1=B4=B5= =E2=86=92 X extending f' such that S(f) =3D g. Taking the transpose of g, we obtain h : LS=E2=96=A1=E1=B4=B5 =E2=86=92 X s= uch that its restriction to LS(=E2=88=82=E2=96=A1=E1=B4=B5) agrees with f' restricted along =CE=B5_{= =E2=96=A1=E1=B4=B5}. We then construct f by lifting [h, f'] through LS=E2=96=A1=E1=B5=8F +_{LS(=E2=88=82=E2=96=A1=E1=B5= =8F)} =E2=88=82=E2=96=A1=E1=B5=8F =E2=86=92 =E2=96=A1=E1=B5=8F, the pushout= application of the counit =CE=B5 : LS =E2=86=92 Id to =E2=88=82=E2=96=A1=E1=B5=8F =E2= =86=92 =E2=96=A1=E1=B5=8F, which is a trivial cofibration by (4.). References. [1] Cohen, Coquand, Huber, M=C3=B6rtberg. Cubical Type Theory: a constructi= ve interpretation of the univalence axiom. https://arxiv.org/pdf/1611.02108 [2] Kapulkin, Voevodsky. Cubical approach to straightening. http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straightenin= g.pdf [3] https://arxiv.org/pdf/1805.04126 --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --000000000000e86c3b0570e717a8 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
When computing homotopy groups of spheres i= n a version of cubical type theory, one might wonder whether this says anyt= hing about the corresponding homotopy groups of spheres in standard homotop= y types; a priori, it might happen that we get different homotopy groups. T= hierry Coquand has answered this question positively for CCHM [1] cubical t= ype theory without reversals (from here on simply referred to as CCHM): giv= en numbers n, k, a=E2=82=81, =E2=80=A6, a=E2=82=9C, if we can derive =E2=8A= =A2 =CF=80=E2=82=96(S=E2=81=BF) =E2=89=83 =E2=84=A4/(a=E2=82=81) =C3=97 =E2= =80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C) in CCHM, then we also have a correspon= ding external isomorphism =CF=80=E2=82=96(S=E2=81=BF) =E2=89=83 =E2=84=A4/(= a=E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C) for the standard= k-th homotopy group of the n-sphere. This email serves to document his arg= ument.

Let =E2=96=A1 denote the full subcategory o= f posets on objects [1]=E1=B4=B5 for I a finite set (=E2=96=A1 can also be = described as the opposite of the Lawvere theory for distributive lattices).= We wite cSet for the category of cubical sets, presheaves over =E2=96=A1. = The presheaf represented by [1]=E1=B4=B5 will be written =E2=96=A1=E1=B4=B5= . Cubical sets form a model category where the cofibrations are the levelwi= se decidable monomorphisms and the fibrations are the maps admitting a unif= orm Kan filling operation in the sense of CCHM. We have a combinatorial des= cription of homotopy groups =CF=80=E2=82=96(X, x=E2=82=80) (as definable in= any model category) of pointed fibrant objects (X, x=E2=82=80) in cSet: th= e underlying set is the quotient of maps =E2=96=A1=E1=B5=8F =E2=86=92 X tha= t are constantly x=E2=82=80 on the boundary =E2=88=82=E2=96=A1=E1=B5=8F by = homotopy (relative to the boundary); the group structure is given by degene= racy and suitable Kan composition of cubes.

Recall= that CCHM has a model in cubical sets. We write =E2=9F=A6-=E2=9F=A7 for th= e interpretation of types and terms and interpret types in the empty contex= t as fibrant cubical sets. Given a pointed type (X, x=E2=82=80) in the empt= y context, we can verify that the points of =E2=9F=A6=CF=80=E2=82=96(X, x= =E2=82=80)=E2=9F=A7 are in bijection with =CF=80=E2=82=96(=E2=9F=A6X=E2=9F= =A7, =E2=9F=A6x=E2=82=80=E2=9F=A7). A bit more (straightforward, though ted= ious) verification shows that the group operations of =CF=80=E2=82=96(X, x= =E2=82=80) defined internally in CCHM have as interpretations maps of presh= eaves whose actions on points correspond to the group operations of =CF=80= =E2=82=96(=E2=9F=A6X=E2=9F=A7, =E2=9F=A6x=E2=82=80=E2=9F=A7). We can define= =E2=84=A4/(a=E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C) in C= CHM so that the interpretation of the type of group elements and the group = operations is (up to isomorphism) constantly at every level the group =E2= =84=A4/(a=E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C). Recall = that S=E2=81=BF in CCHM is defined as a higher inductive type generated by = a base point b and an n-cube whose boundary is constantly b. This is interp= reted as a fibrant replacement 1 +_{=E2=88=82=E2=96=A1=E2=81=BF} =E2=96=A1= =E2=81=BF =E2=86=92 =E2=9F=A6S=E2=81=BF=E2=9F=A7 in cSet. Interpreting the = derivation of =E2=8A=A2 =CF=80=E2=82=96(S=E2=81=BF) =E2=89=83 =E2=84=A4/(a= =E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C) in cubical sets, = we obtain an external group isomorphism =CF=80=E2=82=96(=E2=9F=A6S=E2=81=BF= =E2=9F=A7, =E2=9F=A6b=E2=9F=A7) =E2=89=83 =E2=84=A4/(a=E2=82=81) =C3=97 =E2= =80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C).

The type the= oretic part of the argument is now finished. The rest of the argument relat= es homotopical aspects of cubical and simplicial sets. Let us briefly recal= l the relationship between these two settings. We assume classical logic fr= om here on.

Let =CE=94 denote the simplex category= , the full subcategory of posets on objects [n] for n =E2=89=A5 0. We write= sSet for the category of simplicial sets, presheaves over =CE=94. The pres= heaf represented by [n] will be written =CE=94=E2=81=BF. Recall the Kan mod= el structure on sSet; it is the standard model for homotopy types. The cofi= brations are the monomorphisms and the fibrations are Kan fibrations.
=

Recall from Kapulkin and Voevodsky [2] that simplicial = sets may be seen as a Grothendieck subtopos of cubical sets. We write C : s= Set =E2=86=92 cSet for this fully faithful functor; it can be defined as CA= ([1]=E1=B4=B5) =3D sSet((=CE=94=C2=B9)=E1=B4=B5, A). Its left adjoint S : c= Set =E2=86=92 sSet is the triangulation functor, the cocontinuous extension= of =E2=96=A1 =E2=86=92 sSet sending [1]=E1=B4=B5 to (=CE=94=C2=B9)=E1=B4= =B5. We will also need that S has a further left adjoint L : sSet =E2=86=92= cSet (see [2]), the cocontinuous extension of =CE=94 =E2=86=92 cSet sendin= g the poset [n] to its cubical nerve, the cubical set that at level [1]=E1= =B4=B5 is Poset([1]=E1=B4=B5, [n]) (note that L and C agree on representabl= es). This gives an adjoint triple L =E2=8A=A3 S =E2=8A=A3 C with L and C fu= lly faithful. We include at the end of this text a few useful facts about t= he interaction of the functors L, S, C with the model structures on sSet an= d cSet that will be quoted in the following.

Conti= nuing with the main argument, recall that 1 +_{=E2=88=82=E2=96=A1=E2=81=BF}= =E2=96=A1=E2=81=BF =E2=86=92 =E2=9F=A6S=E2=81=BF=E2=9F=A7 is a fibrant rep= lacement in cSet. By (3.), S is both a left and a right Quillen functor, so= we have that S(1 +_{=E2=88=82=E2=96=A1=E2=81=BF} =E2=96=A1=E2=81=BF) =E2= =86=92 S(=E2=9F=A6S=E2=81=BF=E2=9F=A7) is also a fibrant replacement in sSe= t. Note that S(1 +_{=E2=88=82=E2=96=A1=E2=81=BF} =E2=96=A1=E2=81=BF) =E2=89= =83 1 +_{S(=E2=88=82=E2=96=A1=E2=81=BF)} S(=E2=96=A1=E2=81=BF) (weakly equi= valent to 1 +_{=E2=88=82=CE=94=E2=81=BF} =CE=94=E2=81=BF) presents the n-sp= here in simplicial sets. So S(=E2=9F=A6S=E2=81=BF=E2=9F=A7) really is a fib= rant model for the n-sphere in simplicial sets. Note that we have the same = combinatorial description of homotopy groups for fibrant pointed objects (X= , x=E2=82=80) in simplicial sets as we did in cubical sets, with the underl= ying set of =CF=80=E2=82=96(X, x=E2=82=80) given by the quotient of maps (= =CE=94=C2=B9)=E1=B5=8F =E2=86=92 X that are constantly x=E2=82=80 on its bo= undary by homotopy and the group structure defined using degeneracy and the= same Kan composition as for cubical sets.

It rema= ins to construct a group isomorphism =CF=80=E2=82=96(=E2=9F=A6S=E2=81=BF=E2= =9F=A7, =E2=9F=A6b=E2=9F=A7) =E2=89=83 =CF=80=E2=82=96(S(=E2=9F=A6S=E2=81= =BF=E2=9F=A7), S(=E2=9F=A6b=E2=9F=A7)). We have a canonical function =CF=80= =E2=82=96(=E2=9F=A6S=E2=81=BF=E2=9F=A7, =E2=9F=A6b=E2=9F=A7) =E2=86=92 =CF= =80=E2=82=96(S(=E2=9F=A6S=E2=81=BF=E2=9F=A7), S(=E2=9F=A6b=E2=9F=A7)) given= by the action of S on morphisms. This is a group homomorphism since S take= s the combinatorial description of the homotopy groups in cubical sets to t= he one in simplicial sets. We are left to show that the function is a bijec= tion. Surjectivity is given by (5.) with f' the constant map on =E2=9F= =A6b=E2=9F=A7. For injectivity, consider maps u, v : =E2=96=A1=E1=B5=8F =E2= =86=92 =E2=9F=A6S=E2=81=BF=E2=9F=A7 constantly =E2=9F=A6b=E2=9F=A7 on their= boundary such that S(u) and S(v) are related by a homotopy H : =CE=94=C2= =B9 =C3=97 S=E2=96=A1=E1=B5=8F =E2=86=92 S(=E2=9F=A6S=E2=81=BF=E2=9F=A7) th= at is constantly S(=E2=9F=A6b=E2=9F=A7) on S(=E2=88=82=E2=96=A1=E1=B5=8F). = A lift of H to a homotopy between u and v (relative to their boundary) is t= hen given by (5.) with f' given by u and v on two opposing sides and co= nstantly =E2=9F=A6b=E2=9F=A7 elsewhere and g given by H.

Remarks:
- Recall that there is more structure in a standa= rd homotopy type than just its list of homotopy groups. It seems the above = argument also applies to operations involving multiple groups simultaneousl= y, for example the action of =CF=80=E2=82=81 on =CF=80=E2=82=99, as long as= we can combinatorially describe these operations using cubical filling in = the same manner in both cubical and simplicial sets.
- The argume= nt generalized from spheres to other finite cubical cell complexes.

Appendix.

(1.) L preserves cofib= rations and weak equivalences.
Using cocontinuity of L, one sees = that L(=E2=88=82=CE=94=E2=81=BF) is the subobject of L(=CE=94=E2=81=BF) tha= t at level [1]=E1=B4=B5 contains the non-surjective poset maps [1]=E1=B4=B5= =E2=86=92 [n]. By cocontinuity, since L sends boundary inclusions to cofib= rations, it preserves cofibrations. For preservation of weak equivalences, = by Ken Brown's lemma and cocontinuity, it will suffice to show that L s= ends horn inclusions to weak equivalences. Using cocontinuity and 2-out-of-= 3, this can be further reduced in the standard way to showing that L sends = representables to weakly contractible objects. Recall that L[n] is the cubi= cal nerve of the poset [n]. Note that [n] has an initial object, hence is h= omotopy equivalent to 1. Applying the cubical nerve, we get a homotopy equi= valence between L[n] and 1.

(2.) S preserves cofib= rations and weak equivalences.
As a right adjoint, S preserves mo= nomorphisms (i.e. cofibrations). It also preserves products and pushouts an= d sends the interval in sSet to the interval in cSet. Thus, it sends prism-= style generating trivial cofibrations in sSet to trivial cofibrations in cS= et. By cocontinuity, it preserves all trivial cofibrations. By Ken Brown= 9;s lemma, it preserves weak equivalences.

So we o= btain:
(3.) both adjunctions L =E2=8A=A3 S =E2=8A=A3 C are Quille= n adjunctions.

In particular, S preserves all thre= e classes of the model structure.

(4.) The pushout= application (Leibniz application) of the counit =CE=B5 : LS =E2=86=92 Id t= o the boundary inclusion =E2=88=82=E2=96=A1=E1=B4=B5 =E2=86=92 =E2=96=A1=E1= =B4=B5 is a weak equivalence.
We generalize the claim to any face= lattice subobject M =E2=86=92 =E2=96=A1=E1=B4=B5. Using cocontinuity of LS= and closure properties of weak equivalences and trivial cofibrations, if t= he claim holds for two such subobjects M=E2=82=81 and M=E2=82=82 as well as= their intersection, then also for their union. Thus, it remains to prove t= he claim for face map inclusions =E2=96=A1=E1=B4=B6 =E2=86=92 =E2=96=A1=E1= =B4=B5 and the empty subobject 0 =E2=86=92 =E2=96=A1=E1=B4=B5. Using cocont= inuity and closure properties once more, this reduces to the claim just for= 0 =E2=86=92 =E2=96=A1=E1=B4=B5. So we need to prove that =CE=B5_{=E2=96=A1= =E1=B4=B7} : LS=E2=96=A1=E1=B5=8F =E2=86=92 =E2=96=A1=E1=B5=8F is a weak eq= uivalence, i.e. that LS=E2=96=A1=E1=B4=B7 is weakly contractible. This can = be seen via an explicit contracting homotopy based on the initial vertex. A= lternatively, we may proceed as before and generalize the claim to LN where= N is a union of injections =CE=94=E1=B5=90 =E2=86=92 (=CE=94=C2=B9)=E1=B4= =B7 that preserve the initial and terminal vertex. Using cocontinuity of L = and closure properties of weak equivalences and trivial cofibrations, the c= laim reduces to the case of L=CE=94=E1=B5=90, which we already know from (1= .).

Note that the lack of a Reedy category structu= re on =E2=96=A1 prevents us from using the preceding statement to show that= =CE=B5 is generally valued in weak equivalences.

= Note also that those cubical sets local (in the 1-categorical sense) with r= espect to =CE=B5_{=E2=96=A1=E1=B4=B5} for all I are exactly the sheaves of = Kapulkin and Voevodsky [2], i.e. the cubical sets coming from a simplicial = set under application of C.

(5.) Let X =E2=88=88 c= Set be fibrant; given f' : =E2=88=82=E2=96=A1=E1=B4=B5 =E2=86=92 X and = g : (=CE=94=C2=B9)=E1=B4=B5 =E2=86=92 SX such that S(f') is g restricte= d to its boundary, there is f : =E2=96=A1=E1=B4=B5 =E2=86=92 X extending f&= #39; such that S(f) =3D g.
Taking the transpose of g, we obtain h= : LS=E2=96=A1=E1=B4=B5 =E2=86=92 X such that its restriction to LS(=E2=88= =82=E2=96=A1=E1=B4=B5) agrees with f' restricted along =CE=B5_{=E2=96= =A1=E1=B4=B5}. We then construct f by lifting [h, f'] through LS=E2=96= =A1=E1=B5=8F +_{LS(=E2=88=82=E2=96=A1=E1=B5=8F)} =E2=88=82=E2=96=A1=E1=B5= =8F =E2=86=92 =E2=96=A1=E1=B5=8F, the pushout application of the counit =CE= =B5 : LS =E2=86=92 Id to =E2=88=82=E2=96=A1=E1=B5=8F =E2=86=92 =E2=96=A1=E1= =B5=8F, which is a trivial cofibration by (4.).

Re= ferences.

[1] Cohen, Coquand, Huber, M=C3=B6rtberg= . Cubical Type Theory: a constructive interpretation of the univalence axio= m. https://arxiv.org/pdf/1611.= 02108
[2] Kapulkin, Voevodsky. Cubical approach to straighten= ing. http://uwo.ca/math/faculty/kapulkin/papers/cubical-a= pproach-to-straightening.pdf

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--000000000000e86c3b0570e717a8--