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-wr1-x437.google.com (mail-wr1-x437.google.com [IPv6:2a00:1450:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d1b13398 for ; Wed, 18 Sep 2019 16:27:09 +0000 (UTC) Received: by mail-wr1-x437.google.com with SMTP id a4sf184551wrg.8 for ; Wed, 18 Sep 2019 09:27:09 -0700 (PDT) ARC-Seal: i=3; a=rsa-sha256; t=1568824029; cv=pass; d=google.com; s=arc-20160816; b=Sk3EDdgK7hzYL5w5Ybr44yKdaau6iAT6i1loAMs+4ytoMAjY4aNQBddDGsNiUnyEmD mjpbPsy134zcLTbR76mOSYJOPnxO7l5VVuUVtiys+1F9Tgl+11DxouJyi+35S4jbZhHJ TStm5HGPSJ785rBLGoNzfMk2VH8418CcG34kTcHHJ1aW5o1d3DIzPRkkb8l2Zxq3y4rk xWGQMi9xedP0Z40Vvzxm04uvypLatkv1LDrwMmBabdZXuJk0GBnS7BaRhBFol5ABYM0L +kdzp2LWJGXOc7w5FFSOS1rR/CFyOGXIHG2v7g16CmLqLM/KLEaf+yr25/zYBDHmSAHz vqlw== ARC-Message-Signature: i=3; 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-transfer-encoding :content-id:content-language:accept-language:in-reply-to:references :message-id:date:thread-index:thread-topic:subject:cc:to:from:sender :dkim-signature; bh=KRYJfGQJNUqcK/5ovFlVFuUfFfblVtqSDextIuhqZpw=; b=g0IKcrMQ3XuSUrVZ/xAs4QZ9NIYpp52ShvcJNvSQovbo6q9Xb4Wr1qzw6g24HQHElr /m22g0NyNW8NYoyeQZkroPNhJ8s6qJXHVqNZymY+r8cJ4cD5DbueuUFEHMdm4xwmLaTO K7V+L5ZmDR0CeS0At8t9ie2rFXWxd4oRWumOv7Czs7MZCrHXKld0GwjevDWrQZgT8ck9 neqnhprO8GIkomAP33RvHNtXeGhXHu/o4mfxY8aAnfDFifT/AFN9B9v2CRTBwPxIdNpD 48rpLkm/GnvBgdREEDHi9eyO1+rKMkfXm1PjSu28vwewqXPlowsge6y/Fets+7q/36rU F22g== ARC-Authentication-Results: i=3; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=vVjvapuP; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.77.118 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:from:to:cc:subject:thread-topic:thread-index:date:message-id :references:in-reply-to:accept-language:content-language:content-id :content-transfer-encoding:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=KRYJfGQJNUqcK/5ovFlVFuUfFfblVtqSDextIuhqZpw=; b=U8xvUH5T9f04t7FiddZTrUgHIIGMQg3MX/+0sHswhGwla9eJkSRkKGefpklhCc9fjx RnxUFYbQtPptisiX+3bjdiirCeZ5wpepHfEbE3VDydJ5syi7qMiziillA77dVKr1McmY fHaKWkmnvPReKHdaWkipU3P1OxDzngnqnfYm0XJuvxws8R+J6C+nS2QGkACkTwieMi4l A4tCzo8rZUuYngU9x7Z3aZ2RXJIJV2t6vQMtFUbJm/q28g1kCsS0rsfWWv7x+RhtksFo /pcd0qje1wh8nBiXC+kqZNbCmbTgBvisUErimESTBjHvjXQ+ZEMmS9pFyhLvflZ4alNr T3xQ== 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:cc:subject:thread-topic :thread-index:date:message-id:references:in-reply-to:accept-language :content-language:content-id:content-transfer-encoding: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=KRYJfGQJNUqcK/5ovFlVFuUfFfblVtqSDextIuhqZpw=; b=I5Dd00PNzOWyRtyTBoopE38tCTjIT7TUGXsq6y9TAzT5yZ2AsZuEa1IOKSBrokJPaZ aTBRZxpc09Ia4dxp8hMQggRGOds3zhyeCU6MHJcy0hZFuD9Za0ALibRg7UJTOvm7Ox6J BsjMC6qZXYA/snHVlMvi3HZyTIfYrPFE5qZo1hFwLp/b3vtMZD9Iqru9zC7hR2+oqJXn CkglGdNrMsW0YtovngLGO4ZAWgiKYegjg4RYx39RzVD9py38SU7v4lrwmkVoo5PneqU+ Hu4X7eWqKMXJr+oeY+W6uwiZvUW284ZLd7/dRnxkeoEG/ed/8CTIWlc8NSqbpnz1FLdD JwLA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX+AfD0YplfQHaEI9j4Saky48SQne1yQ9/HoBQn9f5jDv21lIpw jmUU01fC5j5i+SJktaIsLc0= X-Google-Smtp-Source: APXvYqzVihTwyKpQYviIQldfx6c10//geeI1KfcUAOpxClRIkjwxRHT75bpq3BtU0BeIG2MosddALg== X-Received: by 2002:adf:ce04:: with SMTP id p4mr4042442wrn.130.1568824029190; Wed, 18 Sep 2019 09:27:09 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a05:600c:214a:: with SMTP id v10ls153969wml.1.canary-gmail; Wed, 18 Sep 2019 09:27:08 -0700 (PDT) X-Received: by 2002:a7b:c156:: with SMTP id z22mr3867268wmi.142.1568824028655; Wed, 18 Sep 2019 09:27:08 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568824028; cv=pass; d=google.com; s=arc-20160816; b=hzoYRD2b2kgMm0UcsdSu6ffsS8F4usYon69U9l843GkXpz5iqmVSvnUsRjgQZVJbMy 4mY7GWYrukcK855KY1Ikq0APe5KQpEzL+dkZkNoB5D02q9CZ9vWWkz4NX1rmNThRixlK EUJVhTtpM2xaLpmm7E0Xs6JBksXDTEJCLouMJrBKJVhTsI5eW7Dma7d18EvxEsuZtR/w 30fjzwCzaBmujh1e+pYP+p1shrIg076Fmdxevx/LjA+okqpkJjv0F8ssS7aAUd2zI4N7 j1JVZXGoyxrrjcD7re4NEr7mPkIkyjDAWjrwmf9vM8etis+0GWVkSc8LA+12jXzSTp2p 8qrg== ARC-Message-Signature: i=2; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-id:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:dkim-signature; bh=t2GKpg/wjnuLTiDYUmb3phGpI4tCa9ENb+h4kzz/Jj0=; b=PJoTlaUiP97nXy70rAlmqmMgkPJrC6xB7zbzmxbE2lS/w5+H/V2MFHJ+U1bfXqsQke zyxcYnW3n3TZindJQM20PXNfzy4MjkWn1rd5ef3BGQtzM0uJXOoBhSDwNR8OhCiM8/eC pI/rR6wsV8EL7QEdo7lVJL2qFmKfwpL/Dztmamsb3prQ5V3LmQG7DrGZ+VsrG0HN6g7o XaA6fneyd6HL9GwC6x15w/ZD+TwyPDjqDyCl3FSCEn3cHqAfmOuCBq7KGena04ofYKag vW7WWDx2L51Kpv2q967U4BEjzkoIeDe3IyHSPkCKi+FLpqEDk4yzlzCwtB+4/O+VDeYE VX5Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=vVjvapuP; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.77.118 as permitted sender) smtp.mailfrom=dlicata@wesleyan.edu Received: from NAM02-SN1-obe.outbound.protection.outlook.com (mail-eopbgr770118.outbound.protection.outlook.com. [40.107.77.118]) by gmr-mx.google.com with ESMTPS id 5si497941wmf.1.2019.09.18.09.27.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-SHA bits=128/128); Wed, 18 Sep 2019 09:27:08 -0700 (PDT) Received-SPF: pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.77.118 as permitted sender) client-ip=40.107.77.118; ARC-Seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=n6hh2An9LZkt8M7+68SsnZM7MUcOmQ/8VUmpWta3Tu73mKl2Pbemtuv+mbh3/O/yU9UzTtfESqpFtuRmFz5s0D27lvNDtE2xxjE2sy51YO3SY1Eud2bZZOktzmfiae0A8R4eRS5PSRl+sNvp0s9i0DIUamwZbfwCj+b7/OS4FiLyPeLwt2LRL17UnGvtbUM7Xemj9vvA/WSG4AZ5c1uUBUQFvsry/gLpWB8OeMYqVmt3wktYW2RUApW37Yl1Wv+QgfdngIAz5cLhtUuQ7LYSo0OLL6WF3HEN8kQ0CjcqJJJfVAXxL78TNhQRQ2XIglxmGSe9AxRcIj9/oL9M47Irqw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=t2GKpg/wjnuLTiDYUmb3phGpI4tCa9ENb+h4kzz/Jj0=; b=NL0JpMWF0DmO5br8m1UYmk9+rqNzndDIWMXPFPyg3GE3mJqNs4eJ8oBHOyIlbOri+5YG2ssIGh/JMDSQpqdjHYUMtqOOSPq4IrU9sAVAextr4ZKYXIYSRhYz+O4q0j+jCT6FUShmTaENGf0vgDvvwW6vglYa/ak8TiwWG7ScM9VRbRnERBQrzi+1fCAh/TedO/VTQ7Lnsx7MaWsTzNYLHUA2Rca3SvjtDkHiGW6oBoEhNT9iSydw2OMxDFgnCwt4oZ+FktDQ6DGONfsn98sdYD51vZxnyMJw3GyvNbuHCjXG2PiD21Di02Rtk565AsV94bPsR8VYwnq3ymkbfEKe0A== ARC-Authentication-Results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=wesleyan.edu; dmarc=pass action=none header.from=wesleyan.edu; dkim=pass header.d=wesleyan.edu; arc=none Received: from BYAPR04MB4597.namprd04.prod.outlook.com (52.135.237.151) by BYAPR04MB4680.namprd04.prod.outlook.com (52.135.238.155) with Microsoft SMTP Server (version=TLS1_2, cipher=TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384) id 15.20.2263.21; Wed, 18 Sep 2019 16:27:05 +0000 Received: from BYAPR04MB4597.namprd04.prod.outlook.com ([fe80::a123:d7dd:1dd1:a5d4]) by BYAPR04MB4597.namprd04.prod.outlook.com ([fe80::a123:d7dd:1dd1:a5d4%7]) with mapi id 15.20.2263.023; Wed, 18 Sep 2019 16:27:05 +0000 From: "Licata, Dan" To: =?utf-8?B?QW5kZXJzIE3DtnJ0YmVyZw==?= CC: Homotopy Type Theory Subject: Re: [HoTT] Different definitions of Sn Thread-Topic: [HoTT] Different definitions of Sn Thread-Index: AQHVbZIHskWAfOGISkmXvGbyYLgwpKcxHAaAgAAHx4CAADJjgIAASnyA Date: Wed, 18 Sep 2019 16:27:05 +0000 Message-ID: References: <6c150b9c-fba6-47c1-2a6d-975b90f64638@gmail.com> In-Reply-To: Accept-Language: en-US Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [24.60.108.192] x-ms-publictraffictype: Email x-ms-office365-filtering-correlation-id: 0a09ab57-ea1d-4826-b8f3-08d73c550b23 x-microsoft-antispam: BCL:0;PCL:0;RULEID:(2390118)(7020095)(4652040)(8989299)(4534185)(4627221)(201703031133081)(201702281549075)(8990200)(5600167)(711020)(4605104)(1401327)(2017052603328)(7193020);SRVR:BYAPR04MB4680; x-ms-traffictypediagnostic: BYAPR04MB4680: x-ms-exchange-purlcount: 3 x-microsoft-antispam-prvs: x-ms-oob-tlc-oobclassifiers: OLM:8882; x-forefront-prvs: 01644DCF4A x-forefront-antispam-report: SFV:NSPM;SFS:(10019020)(4636009)(136003)(376002)(346002)(39850400004)(366004)(396003)(199004)(189003)(53754006)(26005)(186003)(305945005)(88552002)(6506007)(6436002)(786003)(102836004)(76176011)(478600001)(966005)(316002)(14454004)(53546011)(99286004)(66066001)(8936002)(81156014)(8676002)(1411001)(81166006)(25786009)(4326008)(2906002)(3846002)(6306002)(256004)(6486002)(71200400001)(6116002)(6916009)(229853002)(6512007)(7736002)(86362001)(66946007)(6246003)(71190400001)(76116006)(36756003)(476003)(2616005)(446003)(64756008)(11346002)(75432002)(66476007)(91956017)(486006)(14444005)(66574012)(33656002)(5660300002)(66446008)(66556008);DIR:OUT;SFP:1102;SCL:1;SRVR:BYAPR04MB4680;H:BYAPR04MB4597.namprd04.prod.outlook.com;FPR:;SPF:None;LANG:en;PTR:InfoNoRecords;A:1;MX:1; received-spf: None (protection.outlook.com: wesleyan.edu does not designate permitted sender hosts) x-ms-exchange-senderadcheck: 1 x-microsoft-antispam-message-info: UX4skWft9O674Gm4pqfx98Wmrr9JeXt9d0KODz5yiQTbr3tnNFCnocIehcFFNe6Xpo4JthHpXwiV0bwe+beR6dV1tMVrLPQPSgHK9FqZ6Yaif0VpSCtOgTRVzUUuOujoMFmJ2DgcvpVIKgjbH6hXU6vuGH5mZYVfiStwiTvrAUHyHzUCXfG7aO2RKC7qsCwLM1zvJaWV/1Il6mo0tXSsqDYHNUh+f/G3yC3K7apQcVGU3WdF+Pw+WyVhIvEr/tYhIl8VJSJr0G4rmalfrL7nZVbW6AD5W0RyMsDZ8t+BohgOAJLSMB9W1ChoXcr/xo8rbnNns0teX8xcgKRSO/sX5VhVkZ730hNQ8ikZYgB5jniwV14McVwIV1akXUIA6vzsD1rDPyqjfgqFKd7oc1juB9o49P3KaAQ+5uO9vRRT7to= x-ms-exchange-transport-forked: True Content-Type: text/plain; charset="UTF-8" Content-ID: Content-Transfer-Encoding: quoted-printable MIME-Version: 1.0 X-OriginatorOrg: wesleyan.edu X-MS-Exchange-CrossTenant-Network-Message-Id: 0a09ab57-ea1d-4826-b8f3-08d73c550b23 X-MS-Exchange-CrossTenant-originalarrivaltime: 18 Sep 2019 16:27:05.1532 (UTC) X-MS-Exchange-CrossTenant-fromentityheader: Hosted X-MS-Exchange-CrossTenant-id: a9fd6c79-6d71-49f3-9111-0c8e591dc3d1 X-MS-Exchange-CrossTenant-mailboxtype: HOSTED X-MS-Exchange-CrossTenant-userprincipalname: 4r18TpOTUAccBb5mL1hqLNtmQk7ggzFZY1viJGJElgsrm/F2UQK7QUcRbB8oQqKfY254sXPmpdVteh1te7pPoA== X-MS-Exchange-Transport-CrossTenantHeadersStamped: BYAPR04MB4680 X-Original-Sender: dlicata@wesleyan.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@wesleyan.edu header.s=selector2 header.b=vVjvapuP; arc=pass (i=1 spf=pass spfdomain=wesleyan.edu dkim=pass dkdomain=wesleyan.edu dmarc=pass fromdomain=wesleyan.edu); spf=pass (google.com: domain of dlicata@wesleyan.edu designates 40.107.77.118 as permitted sender) smtp.mailfrom=dlicata@wesleyan.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: , Thanks Anders. To be clear, I don=E2=80=99t think we have any schemas or s= emantics of HITs that accept this definition of S^n (with an n-loop for an = internally-specified n) in any non-cubical settings either; at the time, I = was thinking of it more as exploring what you can do with the definition. = Proving the two definitions equivalent should be the same (modulo which def= initional equalities you get) as implementing the one-n-loop rules in terms= of suspensions, so that would be one way to justify these rules. =20 Also, the proof of pi_n(S^n) =3D Z that Guillaume mentioned, which predated= Freudenthal, is a lot more work than the one that you get from Freudenthal= , so I=E2=80=99m not sure we have any motivating examples for why the one-n= -loop definition is better than the suspension definition for arbitrary n. = =20 -Dan > On Sep 18, 2019, at 8:00 AM, Anders M=C3=B6rtberg wrote: >=20 > Let me elaborate a bit on my answer. One might naively try to copy Dan an= d Guillaume's definition and write the following in Cubical Agda: >=20 >=20 > Omega : (A : Type=E2=82=80) =E2=86=92 A =E2=86=92 Type=E2=82=80 > Omega A a =3D (a =E2=89=A1 a) >=20 > itOmega : =E2=84=95 =E2=86=92 (A : Type=E2=82=80) =E2=86=92 A =E2=86=92 T= ype=E2=82=80 > itOmega zero A a =3D Omega A a > itOmega (suc n) A a =3D itOmega n (Omega A a) refl >=20 > data Sn (n : =E2=84=95) : Type=E2=82=80 where > base : Sn n > surf : itOmega n (Sn n) base >=20 >=20 > However Agda will complain as surf is not constructing an element of Sn. = This might seem a bit funny as Cubical Agda is perfectly happy with >=20 >=20 > data S=C2=B3 : Type=E2=82=80 where=20 > base : S=C2=B3=20 > surf : Path (Path (base =E2=89=A1 base) refl refl) refl refl=20 >=20 >=20 > But what is happening under the hood is that surf is a constructor taking= i, j, and k in the interval and returning an element of S^3 with boundary = "base" whenever i, j and k are 0 or 1. In cubicaltt we can write this HIT i= n the following way: >=20 >=20 > data S3 =3D base > | surf [ (i=3D0) -> base > , (i=3D1) -> base > , (j=3D0) -> base > , (j=3D1) -> base > , (k=3D0) -> base > , (k=3D1) -> base ] >=20 >=20 > The problem is then clearer: in order to write the surf constructor of Sn= we would have to quantify over n interval variables and specify the bounda= ry of the n-cell. This is what that is not supported by any of the cubical = schemas for HITs. >=20 > -- > Anders >=20 > On Wednesday, September 18, 2019 at 11:00:22 AM UTC+2, Guillaume Brunerie= wrote: > Hi,=20 >=20 > We give a definition of S^n with one point and one n-loop by=20 > introduction/elimination/reduction rules in our paper with Dan Licata=20 > (https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can be=20 > implemented in Agda (so Kristina=E2=80=99s question can be formulated and= can=20 > presumably be formalized in Agda) but I don=E2=80=99t think we actually p= roved=20 > it.=20 >=20 > Best,=20 > Guillaume=20 >=20 > Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg :=20 > >=20 > > Hi Kristina,=20 > >=20 > > We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda:=20 > > https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda= =20 > >=20 > > However, I don't think we can even write down the general version of=20 > > S^n as a type with a point and an n-loop with the schema implemented=20 > > in Cubical Agda. As far as I know no other schema for HITs support=20 > > this kind of types either.=20 > >=20 > > --=20 > > Anders=20 > >=20 > > On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova=20 > > wrote:=20 > > >=20 > > > Hello everybody,=20 > > >=20 > > > Is it worked out somewhere that the two definitions of Sn as a=20 > > > suspension on one hand and a HIT with a point and an n-loop on the ot= her=20 > > > hand are equivalent? This is also an exercise in the book. I know=20 > > > Favonia has some Agda code on spheres but I couldn't find this result= in=20 > > > there.=20 > > >=20 > > > Thanks,=20 > > >=20 > > > Kristina=20 > > >=20 > > >=20 >=20 > --=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= email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgi= d/HomotopyTypeTheory/db712ad2-396f-4328-bb73-898dcb956834%40googlegroups.co= m. --=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. To view this discussion on the web visit https://groups.google.com/d/msgid/= HomotopyTypeTheory/DBF368F2-295C-4175-93F2-1EA01D49B95D%40wesleyan.edu.