From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBC4PDJ5VRELBBFNGVHNAKGQE3JMQPMY@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.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-lf0-x238.google.com (mail-lf0-x238.google.com [IPv6:2a00:1450:4010:c07::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b367898f for ; Sat, 14 Jul 2018 19:46:30 +0000 (UTC) Received: by mail-lf0-x238.google.com with SMTP id b26-v6sf8241221lfa.14 for ; Sat, 14 Jul 2018 12:46:30 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531597589; cv=pass; d=google.com; s=arc-20160816; b=h7YU4T3wmT2bSnmauBANT6CzW4C0U9YY18/8Az8SzS1qxEWSUxGtPbCxMcjBCnJBAr aj72Vwf9beVqCQ4sgSTtw54lEtPqf2Nw6lK6mTNaoP0vR7SdGmApaC8tt9hdtMl7+urW gf1qkehEr3qWTQMgBiZGtGtn+562Ae8K1//80bW6b811HLpwnEG0oogvS/eGjq5BhXAm GOet7YwH3NuZ3es5nF+x+LAOsnzGTw3zUoHdI29xqYsxVO5j8xq7RvPZ6l8i1FG4nm2G reimfylrQd752NiUIR6anaSPg6PxmXjNpkeQ5+owexqvEF8rJB/owyU2SiZwcIAmR+HW KCmw== 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:mime-version:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:to:from:arc-authentication-results :arc-message-signature:sender:dkim-signature :arc-authentication-results; bh=oOsGvMl5jnENXA4GQGHYlTCx+WX2Wn9SMj2mXTiP0DI=; b=RfNhrLDOuQonJuhIVIwrhMp8bGENnQBTQgRwrW8A0ckpHKXtGqn3k4/5bQ9T4chwL+ vY/jRuWoqs0QrfBUfHRMmBhVok0I1rhSJ8tpV5PtWTLXuA1rNwCS5tb2pDqgKlBJFX1C 6vkPUIQRXCBV0m9IkN/+QPP6jXOoEnryt+gGEuEHorT8Sucn3thRas+oJKf7SNB5nSCe L5/hP7P6Nj9H3VXPp/nclfBV+PvWU+JX2WpyF46KjRvq3+zKRQQsGrqRGGK246B12rj0 rfDWbgnXqE+gm4ISqpX4BK1Q9JsXeX6xJcndV0FJjabzYPyX5+BwYgn44Acgn1mvEXQn MSaQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.136 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) smtp.mailfrom=Thierry.Coquand@cse.gu.se DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language :mime-version:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=oOsGvMl5jnENXA4GQGHYlTCx+WX2Wn9SMj2mXTiP0DI=; b=asxxpCXdHdiwHwJrZcVvOu+x/xBvawbmMzhWl1wYFUqXVzZPAeOXVQIwZ/887HygKq IKfR2c9MsKT0IhTtbMrOOyhrFX5UR+/Ihq2IC0XLEWudqshhKnzICntczHO8bXtnWYWg 9PJ40ohD7iWmr5xJUBgy3vRfe0mvP8TmC6nw3WvIKqKaZuLT6BfXZdLBU4BOFoRB9Qyz lj7zzj/KfbMODU/yQjW3VrX6yztuEox1iz+RMWxRh4cppvbw37wIX7nWdWLLvmknKCKL O7PL9C3PRqj1jOD7BiBTW1MAO0tidAVvlM8TEvri8ldmtyVuQLKH/pY9D3Zssim1oSwR /olQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:from:to:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:mime-version: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=oOsGvMl5jnENXA4GQGHYlTCx+WX2Wn9SMj2mXTiP0DI=; b=UaLjqkbRWw+MsRdT4LSijAdxHfo09bahDQN9D3xSlsv0ZuAjmX0h43t6SI3nQjnSVX 5Q6evk2wv5ta8CfcsLztTKR+SyQTEihYQpkT2w6mcMr6yhuQSu1nW6hNCkXKYzYRz1ql pZVEa1rutWf2XLjWB20kB3aLyhKFrUictwMfyO7qGK2EvA9QQfAHPu3y8tQTJpAYTgQi SiqrFgiNh7gZvBGpRowUxdSZLkMQn+HShuKkjZ7IjsWvx9koyGSW9IdSB/Mjpg92k3FG wye/A1GGqHScbRw3Sxf0NBo43c4fCFlWH3FQWopCT2OnYWNk+PqyF168CfJ5Lp8yVUiV H/yw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlHlxB932yQ/yBNdi6mz2NW7+jtBbjgO3o2ja27bz6lcwzhd+ZAT k0FTUCD/VwwqDzv9bH5WnGc= X-Google-Smtp-Source: AAOMgpdzvbm4MQtsTPK2djiWz8+4Gn41JLl3y6SMYAUWY+j0yb5T3V5H8oaSRli60TrgiQlh62CYyg== X-Received: by 2002:a2e:954a:: with SMTP id t10-v6mr72924ljh.6.1531597589382; Sat, 14 Jul 2018 12:46:29 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:84cf:: with SMTP id q15-v6ls1094938ljh.6.gmail; Sat, 14 Jul 2018 12:46:28 -0700 (PDT) X-Received: by 2002:a2e:380e:: with SMTP id f14-v6mr540752lja.14.1531597588670; Sat, 14 Jul 2018 12:46:28 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531597588; cv=none; d=google.com; s=arc-20160816; b=KrsMa2TpyQdTQCsu4wQovvs5EzypoRuCmXe/C2i3Wa5OZZkEIGV/17dNUWbHEtmmes JWA9w5YogzYqbhjRMhCVJTl8/6st+BDu/S43WAvtdgz19x7D6LLlpAYggH7+MZaevrwI OY0wVmPPaLkbO0pvPY4VFzLZFdv8loofBC9t/JK64F5YiF4fgTFfIBMowr7mfATFuV89 CA2R7MfpLlLrHurzIXaz2H07dtDPjXptKNKYUsSj3X0ynLPBOw0eaLLnslrTiMgkYzbd owvEddi75r7k64nCB6RS2ej3+5Bu8BXp6zx1NY04EXhbu6nQwscpEOfF6NBBUI2kHTRl eyTw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-language:accept-language:in-reply-to :references:message-id:date:thread-index:thread-topic:subject:to :from:arc-authentication-results; bh=8bjhjhHM3KzCzI4T1knSHdtO7BqJ3/7Dam2I26+XoW8=; b=CLsxWDrSzi1RUlPlmOEP8L+mndhIq/+DWCLRBWZaFZHNdmb4Lo1W2N+wS97Ne715bJ hUyff89iTv1q9d10AHgDtGjhw8Aep6mBAsAwBPUrT4V8fhyNGdfCBizfrMrvQ5C+fvm4 GCLASR4v0Ektb4hupkvN7Zn5SJQbv9Els5cjBVfG+4XnEtbSAJKnBDJ5i8pMwyl+00VG gL3OgPii19DkcmHtS0vnU4dqFQpQzOo5VPlVMu4KwcfaNaep0jdGstuT5Vx4TTJG5nkT t9EjyTm6h3hVnUybcM+GfexgFNOIkuOMQtkbqfUViiZqMGyC9Cso+VupjAp7GUqTA+Zg 2w3Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=neutral (google.com: 129.16.226.136 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) smtp.mailfrom=Thierry.Coquand@cse.gu.se Received: from baratheon.ita.chalmers.se (baratheon.ita.chalmers.se. [129.16.226.136]) by gmr-mx.google.com with ESMTPS id k15-v6si699147ljh.1.2018.07.14.12.46.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Sat, 14 Jul 2018 12:46:28 -0700 (PDT) Received-SPF: neutral (google.com: 129.16.226.136 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) client-ip=129.16.226.136; Received: from tyrell.ita.chalmers.se (129.16.226.132) by baratheon.ita.chalmers.se (129.16.226.136) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_CBC_SHA384_P256) id 15.1.1531.3; Sat, 14 Jul 2018 21:46:27 +0200 Received: from tyrell.ita.chalmers.se ([129.16.226.132]) by tyrell.ita.chalmers.se ([129.16.226.132]) with mapi id 15.01.1531.003; Sat, 14 Jul 2018 21:46:27 +0200 From: Thierry Coquand To: Homotopy Theory Subject: Re: [HoTT] homotopy groups in CCHM cubical type theory Thread-Topic: [HoTT] homotopy groups in CCHM cubical type theory Thread-Index: AQHUGuXHmko5k/8eu0uC9A8un59+kaSO/2AA Date: Sat, 14 Jul 2018 19:46:27 +0000 Message-ID: <06CFC924-6830-4182-8D87-1E3A272D5F1F@chalmers.se> References: In-Reply-To: Accept-Language: en-US, sv-SE Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [129.16.10.245] Content-Type: multipart/alternative; boundary="_000_06CFC924683041828D871E3A272D5F1Fchalmersse_" MIME-Version: 1.0 X-Original-Sender: thierry.coquand@cse.gu.se X-Original-Authentication-Results: gmr-mx.google.com; spf=neutral (google.com: 129.16.226.136 is neither permitted nor denied by best guess record for domain of thierry.coquand@cse.gu.se) smtp.mailfrom=Thierry.Coquand@cse.gu.se 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: , --_000_06CFC924683041828D871E3A272D5F1Fchalmersse_ Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Some further remarks on this message: -the reference [3] should be https://arxiv.org/abs/1805.04126 -we consider Dedekind cubical sets where cofibrations are decidable sieves -in the paper http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straighteni= ng.pdf one result is that we can see simplicial sets exactly as special kind of cubical sets that are sheaves forcing the following 1 =3D x <=3D y \/ y <=3D x The original idea for connecting homotopy groups was to refine the notion o= f fibrant cubical sets by forcing \phi =3D x <=3D y \/ y <=3D x (1) to be a trivial cofibration. This amounts to consider the model where we look only at modal types for the modality X |-> X ^{[\phi]} More generally we can force to be a trivial cofibration also any sieve wh= ich becomes 1 by triangulation in the simplicial set model. (This should be a special case of Bousfield lo= calisation, but all the arguments are effective.) In this way we can prove that homotopy groups coincide in the simplicial a= nd cubical worlds. For instance, for pi_2 we use that x <=3D y <=3D z \/ y <=3D x <=3D z \/ x <=3D z <=3D y \/ z <=3D x <= =3D y \/ y <=3Dz <=3D x \/ z <=3D y <=3D x \/ x =3D 0 \/ x =3D 1 \/ y =3D 0 \/ y =3D 1 \/ z =3D 0 \/ z =3D 1 (2) becomes a trivial cofibration. Christian noticed that (1) or (2) are already a trivial cofibration in the= original cubical set model. (For (1), this is because the map [\phi] -> 1 is an equivalence and = by 3-out-of-2 the inclusion [\phi] in the square has to be an equivalence, hence it is a = trivial cofibration.) More generally, all the maps that were needed to be trivial cofibration fo= r the argument relating homotopy groups can already be shown to be trivial cofibration. So localisation is not needed for this argument. -it also follows from http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straighteni= ng.pdf that C preserves fibrancy. Using the results in https://arxiv.org/abs/1805.04126 Christian could show that the triangulation functor S preserves fibrancy (t= he argument uses classical logic) which was needed to show that S commutes with fibrant replacement. Thierry On 13 Jul 2018, at 22:12, Christian Sattler > wrote: When computing homotopy groups of spheres in a version of cubical type theo= ry, one might wonder whether this says anything about the corresponding hom= otopy groups of spheres in standard homotopy types; a priori, it might happ= en that we get different homotopy groups. Thierry Coquand has answered this= question positively for CCHM [1] cubical type theory without reversals (fr= om 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 we 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 the standard k-th homotopy group of the n-sp= here. 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 o= f 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 cat= egory where the cofibrations are the levelwise decidable monomorphisms and = the fibrations are the maps admitting a uniform Kan filling operation in th= e 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 underlying set is the quotien= t 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 bound= ary); the group structure is given by degeneracy and suitable Kan compositi= on 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 th= e 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 in CCHM have as interpretations maps of pre= sheaves 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 def= ine =E2=84=A4/(a=E2=82=81) =C3=97 =E2=80=A6 =C3=97 =E2=84=A4/(a=E2=82=9C) i= n CCHM so that the interpretation of the type of group elements and the gro= up 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 int= erpreted 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 t= he 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 ar= gument relates homotopical aspects of cubical and simplicial sets. Let us b= riefly recall the relationship between these two settings. We assume classi= cal logic from here on. Let =CE=94 denote the simplex category, the full subcategory of posets on o= bjects [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 writt= en =CE=94=E2=81=BF. Recall the Kan model structure on sSet; it is the stand= ard model for homotopy types. The cofibrations are the monomorphisms and th= e 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 s= Set((=CE=94=C2=B9)=E1=B4=B5, A). Its left adjoint S : cSet =E2=86=92 sSet i= s 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 c= ocontinuous extension of =CE=94 =E2=86=92 cSet sending 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 representables). This gives an adj= oint triple L =E2=8A=A3 S =E2=8A=A3 C with L and C fully faithful. We inclu= de 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 qu= oted 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 fibr= ant replacement in cSet. By (3.), S is both a left and a right Quillen func= tor, 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 i= n 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) (weakl= y equivalent to 1 +_{=E2=88=82=CE=94=E2=81=BF} =CE=94=E2=81=BF) presents th= e 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 obje= cts (X, x=E2=82=80) in simplicial sets as we did in cubical sets, with the = underlying set of =CF=80=E2=82=96(X, x=E2=82=80) given by the quotient of m= aps (=CE=94=C2=B9)=E1=B5=8F =E2=86=92 X that are constantly x=E2=82=80 on i= ts boundary by homotopy and the group structure defined using degeneracy an= d 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 se= ts 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 th= eir 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) 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) i= s then given by (5.) with f' given by u and v on two opposing sides and con= stantly =E2=9F=A6b=E2=9F=A7 elsewhere 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 o= perations 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 cu= bical and simplicial sets. - The argument generalized from spheres to other finite cubical cell comple= xes. 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 p= reservation of weak equivalences, by Ken Brown's lemma and cocontinuity, it= will suffice to show that L sends horn inclusions to weak equivalences. Us= ing cocontinuity and 2-out-of-3, this can be further reduced in the standar= d 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 inter= val in cSet. Thus, it sends prism-style generating trivial cofibrations in = sSet to trivial cofibrations in cSet. By cocontinuity, it preserves all tri= vial 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 equivale= nces 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. This can be seen via an explicit contracting= homotopy based on the initial vertex. Alternatively, we may proceed as bef= ore 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 t= erminal vertex. Using cocontinuity of L and closure properties of weak equi= valences 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 i= n 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 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 liftin= g [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 appli= cation 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/m= ath/faculty/kapulkin/papers/cubical-approach-to-straightening.pdf [3] http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straight= ening.pdf -- 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. --=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. --_000_06CFC924683041828D871E3A272D5F1Fchalmersse_ Content-Type: text/html; charset="UTF-8" Content-ID: <59884EC240FDAB498E940E925B768CBE@chalmers.se> Content-Transfer-Encoding: quoted-printable
 Some further remarks on this message:

 -the reference [3] should be 

htt= ps://arxiv.org/abs/1805.04126

 -we consider Dedekind cubical sets where cofibrations= are decidable sieves

 -in the paper

 http://uwo.ca/math/facul= ty/kapulkin/papers/cubical-approach-to-straightening.pdf

one result is that we can see simplicial sets exactly as sp= ecial kind of 
cubical sets that are sheaves forcing the following 

 1 =3D    x <=3D y   \/    = ;y <=3D x

The original idea for connecting homotopy groups was to ref= ine the notion of fibrant cubical sets by forcing

  \phi =3D x <=3D y \/ y <=3D x (1)

to be a trivial cofibration.

 This amounts to consider the model where we look only= at modal types
for the modality X |->   X ^{[\phi]}
 
 More generally we can force  to be a trivial cof= ibration also any sieve which becomes 1 by triangulation
in the simplicial set model. (This should be a special case= of Bousfield localisation, but 
all the arguments are effective.)

 In this way we can prove that homotopy groups coincid= e in the simplicial and cubical
worlds. For instance, for pi_2 we use that 

 x <=3D y <=3D z  \/  y <=3D x <= =3D z  \/  x <=3D z <=3D y  \/  z <=3D x <= =3D y  \/  y <=3Dz <=3D x  \/  z <=3D y <= =3D x  \/
 x =3D 0 \/ x =3D 1  \/
 y =3D 0 \/ y =3D 1  \/
 z =3D 0 \/ z =3D 1 (2)

becomes a trivial cofibration.

 Christian noticed that (1) or (2) are already a trivi= al cofibration in the original cubical set
model. (For (1), this is because the map [\phi] -> 1 is = an equivalence and by 3-out-of-2
the inclusion [\phi] in the square has to be an equivalence= , hence it is a trivial cofibration.)
 More generally, all the maps that were needed to be t= rivial cofibration for the argument
relating homotopy groups can already be shown to be trivial= cofibration.
So localisation is not needed for this argument.

 -it also follows from 

 http://uwo.ca/math/facul= ty/kapulkin/papers/cubical-approach-to-straightening.pdf

that C preserves fibrancy. Using the results in 

 https://arxiv.org/abs/1805.04126

Christian could show that the triangulation functor S prese= rves fibrancy (the argument uses classical logic)
which was needed to show that S commutes with fibrant repla= cement.

 Thierry

 


On 13 Jul 2018, at 22:12, Christian Sattler <sattler.christian@gmail.com<= /a>> wrote:

When computing homotopy groups of spheres in a version of c= ubical type theory, one might wonder whether this says anything about the c= orresponding homotopy groups of spheres in standard homotopy types; a prior= i, 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 referr= ed to as CCHM): given numbers n, k, a=E2=82=81, =E2=80=A6, a=E2=82=9C, if w= e 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 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 the 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 obje= cts [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 fo= r 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 se= ts form a model category where the cofibrations are the levelwise decidable= monomorphisms and the fibrations are the maps admitting a uniform Kan fill= ing 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 definabl= e in any model category) of pointed fibrant objects (X, x=E2=82=80) in cSet= : the underlying 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 cub= es.

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 ty= pes 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 m= ore (straightforward, though tedious) verification shows that the group ope= rations of =CF=80=E2=82=96(X, x=E2=82=80) defined internally in CCHM have a= s 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 typ= e of group elements and the group operations is (up to isomorphism) constan= tly 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 ba= se point b and an n-cube whose boundary is constantly b. This is interprete= d 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. Th= e rest of the argument relates homotopical aspects of cubical and simplicia= l 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 subcategor= y of posets on objects [n] for n =E2=89=A5 0. We write sSet for the categor= y 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 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 : cSet =E2=86=92 sSet is the triangulation functor, the cocontinuous extensi= on 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 representables). This gives an adjoint trip= le L =E2=8A=A3 S =E2=8A=A3 C with 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 q= uoted 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 &#= 43;_{S(=E2=88=82=E2=96=A1=E2=81=BF)} S(=E2=96=A1=E2=81=BF) (weakly equivale= nt 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 i= n cubical sets, with the underlying set of =CF=80=E2=82=96(X, x=E2=82=80) g= iven by the quotient of maps (=CE=94=C2=B9)=E1=B5=8F =E2=86=92 X that are c= onstantly x=E2=82=80 on its boundary by homotopy and the group structure de= fined 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=A6S=E2=81=BF=E2=9F=A7), S(=E2=9F=A6b=E2=9F=A7)). We have a can= onical 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 homo= morphism since S takes the combinatorial description of the homotopy groups in cubical sets to the one in simplicia= l 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 injec= tivity, 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) on S(= =E2=88=82=E2=96=A1=E1=B5=8F). A lift of H to a homotopy between u and v (re= lative 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 elsewhere and g given by= H.

Remarks:
- Recall that there is more structure in a standard homotop= y type than just its list of homotopy groups. It seems the above argument a= lso applies to operations involving multiple groups simultaneously, for exa= mple 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 argument generalized from spheres to other finite cub= ical 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 subobject of L(=CE=94=E2=81=BF) that at level [1]=E1=B4=B5 c= ontains the non-surjective poset maps [1]=E1=B4=B5 =E2=86=92 [n]. By cocont= inuity, since L sends boundary inclusions to cofibrations, it preserves cof= ibrations. For preservation of weak equivalences, by Ken Brown's lemma and cocontinuity, it will suffi= ce to show that L sends horn inclusions to weak equivalences. Using coconti= nuity and 2-out-of-3, this can be further reduced in the standard way to sh= owing that L sends representables to weakly contractible objects. Recall that L[n] is the cubical nerve of t= he poset [n]. Note that [n] has an initial object, hence is homotopy equiva= lent to 1. Applying the cubical nerve, we get a homotopy equivalence betwee= n L[n] and 1.

(2.) S preserves cofibrations and weak equivalences.
As a right adjoint, S preserves monomorphisms (i.e. cofibra= tions). It also preserves products and pushouts and sends the interval in s= Set 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 Br= own'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 s= tructure.

(4.) The pushout application (Leibniz application) of the c= ounit =CE=B5 : LS =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 s= uch subobjects M=E2=82=81 and M=E2=82=82 as well as their intersection, the= n also for their union. Thus, it remains to prove the claim for face map inc= lusions =E2=96=A1=E1=B4=B6 =E2=86=92 =E2=96=A1=E1=B4=B5 and the empty subob= ject 0 =E2=86=92 =E2=96=A1=E1=B4=B5. Using cocontinuity and closure propert= ies 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. This can be seen via an explicit contract= ing 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 v= ertex. 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 from using the preceding statement to show that =CE=B5 is g= enerally valued in weak equivalences.

Note also that those cubical sets local (in the 1-categoric= al 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 fr= om 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 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 cons= truct 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 Theo= ry: a constructive interpretation of the univalence axiom. https://arxiv.org/p= df/1611.02108
[2] Kapulkin, Voevodsky. Cubical approach to straightening.= http://uwo.ca/math/faculty/kapulkin/papers/cubical-approach-to-straightenin= g.pdf
[3] http://uwo.ca/math/fa= culty/kapulkin/papers/cubical-approach-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 https://groups.google.com/d/optout.

--
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.
--_000_06CFC924683041828D871E3A272D5F1Fchalmersse_--