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.2 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-lj1-x239.google.com (mail-lj1-x239.google.com [IPv6:2a00:1450:4864:20::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id efc9e290 for ; Wed, 18 Sep 2019 09:00:22 +0000 (UTC) Received: by mail-lj1-x239.google.com with SMTP id j11sf1037861ljh.7 for ; Wed, 18 Sep 2019 02:00:22 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568797222; cv=pass; d=google.com; s=arc-20160816; b=NzqM1ArhR9MZ3i+R7JyEYDrKyqtUX884xgDJg+URxAXQszK+p+O2MrrWH3Eb7VzhS6 jbcXGpIB17gaWhT4KQacBK/cdRWOG2gKH/fGM4dUaM5QecA2tV4eM2p1CNwpn44+KCmc jdLS5t50HaCq5sbrZSQFfNIwY9ktXbKYPK4Nh2jOztAmoatjWd/3dvIXrPoMup0xM+8K BPPxIeAgg53gWYCIIYCn0u7MSMRFZe84HENHrfkbFtLBVM4oVj03r4hDNNf5YoJuE6eV X5L/80GrCMMkaZBeLVSy3MdNRO778sNlW5KynYdXGkqeXmadkdeGw/8DHHdzKS8Yh2pS kn8w== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature:dkim-signature; bh=edO5NSij+MAp8Dam7Kn2V6dbXhUeuGNrx16mfLL1TPA=; b=rCFFBfGt7Oa+yFVhPNez0qhAglfSHSCX56BywnYXHj+/1vo8AcpZPAtjJayXsVsRTY +Q0cu96hXVXS3xNOSF1OrGrwA2uB6vblda9Lr2/p1UURJVNS+fUSN56dZTuFqU+wCGTo MllJIIXcVOfdewblfdBuLEDR6oe/wpSumYwKL0Sf2xiU1Hfm9Wg+We0bo47SoqW6yrKQ E6Mx5Ny+2fB2eDDdJ8wzJssvWPpEuI/fthNgGhLbT7s737Rw4uUfTVWe4NaRpUeOXd1K udmvlvzC3hO09PuX+lcvJ2WqVjMmSG7kOpmxHSCTxumufO+7DvxEJq3Nxe+ZTwU/GyNo 6/lg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t9PJ4IFL; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::129 as permitted sender) smtp.mailfrom=guillaume.brunerie@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:references:in-reply-to:from:date:message-id :subject:to:cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=edO5NSij+MAp8Dam7Kn2V6dbXhUeuGNrx16mfLL1TPA=; b=ZoMponxht2y2RCn8M9v8/sYGTLP9npwE6gF+qAOJaZXgldOLz48vZ0UmUPE2xCx0ET VrUBmMpWogXRBWD5pA+FQRE2uZzur4WOvb+7HgsIaqELc00UsyHGoKKBIMTjwebb2M4M mLG3+IORY6Mqpf8pgaXFm5i3B+b5aE6LnotAQmDy+VWEx7WzrdBO1REc1oSmj9O60+IT PoqOyNMLrZMhvNec21Up4btEHvcmOh5N2wGmogpCVc/c0x1KCC7DDs2MJQm61lku7Uyk REOnh7uGojp2IHmQEPyBpz/Cur2befNa9H/xKKriK68fRJF2oVRn5QXmVvjEal1zwwb8 rBMQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=edO5NSij+MAp8Dam7Kn2V6dbXhUeuGNrx16mfLL1TPA=; b=OjugAOqfinUrDasFQOeBpXkVc5spcTpDFTSqzRzURr8Lk5vlF4J5zlKsdUaQi3ooTK aHc9USumrabRk6KdEzdOn7p0kddvKSlv830F5eGa1OsuJztoXvzAPpoXhQbF3trC4y3C xfI7xfox7p2qMPEDfc7y68nMNaGg+YMTcJrK6cgTQErwcGc1DvfViTxadj9C00vc9qRb CpqmYL3NiNYbBJNPUo4a0eBoG2qzV1USy5tFcrXKne1pNGaYFRzHxBvlRmku83DZ5HlQ 92ed1eYIvhl/CerCwzert7Bw+XcjrU7nnDp48BCE7gtA/tIOLRvmPfJ+ayTsEKJvd6bk lubQ== 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:references:in-reply-to:from :date:message-id:subject:to:cc:content-transfer-encoding :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=edO5NSij+MAp8Dam7Kn2V6dbXhUeuGNrx16mfLL1TPA=; b=l12DtNXeryIIE5guQhrfn8Lc4hOmaod3qmI+qFU0ce/HDxSCCsC9PKloqiqqfXUNEd AvO07Y5gj80y/dlNUiU6562ffGoHR37Uu1UbfzOH05ihp/xhnzyLL9ojvghbmRDQuqGG wV7dn1v0y47li3folR6PUne4SvrN4Ms5VAMIJv3MJVR3oJ3+0S3p9y8PgiF0mJnmYAjZ YO6i39OhG0UjbRG79wbLh6pXrBWlF0Ybm+Ad2zruPd9OWTniPwB01T/LRHxfBVYhuO8n q1UtVqRMcRZL5Gysmx3LzcFZTRE0XjT91Y7qYYF14JYhSF+20YInAoWCGZvD3phpYeDr yxuA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAUznFyLP2DtXRlryAZIydN9MVEekJrgt9HHDpXx8RwGjEn5LRT/ y9erDIOXq5A3l1p2chWo6VE= X-Google-Smtp-Source: APXvYqztS7RL6KzQ7HRSJG6QxKPrVYc25p3fSjCuAh7VFMON6RlrgWtrestrpST+oagkhjhakRfsyQ== X-Received: by 2002:a19:6455:: with SMTP id b21mr1524196lfj.167.1568797221955; Wed, 18 Sep 2019 02:00:21 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:934e:: with SMTP id m14ls778198ljh.4.gmail; Wed, 18 Sep 2019 02:00:21 -0700 (PDT) X-Received: by 2002:a2e:6d12:: with SMTP id i18mr1522116ljc.223.1568797221200; Wed, 18 Sep 2019 02:00:21 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568797221; cv=none; d=google.com; s=arc-20160816; b=r4RCjh1q58mG43ACL/ZzQsuTWV3qmNmQWDdvy21gj6EPpgwhxHB11+RFOpz4ZEMfjm HSEL2Mitwm5PFNyrvL9UElxCzSQJvX5YX1uxJhS3BMEiV3zZuff/vDz2O0g2QBMX/Bxd U1qO7N2+6zp0i8ls78ofegZMlGkZbpnAGFfHYSZPfWo8sDSENWfFVHpDY6Br7ue6xcis dsX7j4HoOkDEtuYegnOcsE4hsv3ohuX5qR+GPFx+3BHXIptQ260AZR8mzeRUXnfFjtV/ G9eAOr2dUBshms2DkMD+RBiJWF0H/UFAk42uzBwhgKXHV7xb3Md92Q13Rbk2Vajn1xwB WDzA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=JGyCHFE/nQYH0OTO+Iu7uWLD6NMftoGgQWkUc0EumLg=; b=T+90xWNskXRBY5GWxqVm3dtonc4a8OHVCwl7wRGm4cKc8Lep78Rhp972nyPozCRWkU ew9GUCjeMyiLISNscRngeNuBlS/8FECn7RtW6E0OpRStR/Tbo/FsS20Mnw7k0XcUntKP y+oeX3yx0Mz6uIT3DcmLf44RVE1f1f9bnK1spt40uEO+qHqhclGIzf2m759pnbJrhbwL FDCd5OAPcNcDJNNdEm6m2dOaBYBuYcyFltqsccob8e7RDB3tz6KEDKdVSZJOCSDugLm8 G0bVRtDm6sCVaDkKRN08dkK3aGKFbUgKn19z1SPgt74u1xJugN3DvzoxKoGfmN0cGGx/ /xOg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t9PJ4IFL; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::129 as permitted sender) smtp.mailfrom=guillaume.brunerie@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-lf1-x129.google.com (mail-lf1-x129.google.com. [2a00:1450:4864:20::129]) by gmr-mx.google.com with ESMTPS id c8si412380lfm.4.2019.09.18.02.00.21 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 18 Sep 2019 02:00:21 -0700 (PDT) Received-SPF: pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::129 as permitted sender) client-ip=2a00:1450:4864:20::129; Received: by mail-lf1-x129.google.com with SMTP id x80so5110804lff.3 for ; Wed, 18 Sep 2019 02:00:21 -0700 (PDT) X-Received: by 2002:a19:6556:: with SMTP id c22mr1513830lfj.90.1568797220896; Wed, 18 Sep 2019 02:00:20 -0700 (PDT) MIME-Version: 1.0 References: <6c150b9c-fba6-47c1-2a6d-975b90f64638@gmail.com> In-Reply-To: From: Guillaume Brunerie Date: Wed, 18 Sep 2019 11:00:09 +0200 Message-ID: Subject: Re: [HoTT] Different definitions of Sn To: Anders Mortberg Cc: Kristina Sojakova , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: guillaume.brunerie@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=t9PJ4IFL; spf=pass (google.com: domain of guillaume.brunerie@gmail.com designates 2a00:1450:4864:20::129 as permitted sender) smtp.mailfrom=guillaume.brunerie@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: , Hi, We give a definition of S^n with one point and one n-loop by introduction/elimination/reduction rules in our paper with Dan Licata (https://guillaumebrunerie.github.io/pdf/lb13cpp.pdf), which can be implemented in Agda (so Kristina=E2=80=99s question can be formulated and c= an presumably be formalized in Agda) but I don=E2=80=99t think we actually pro= ved it. Best, Guillaume Den ons 18 sep. 2019 kl 10:32 skrev Anders Mortberg : > > Hi Kristina, > > We have proofs for S^0, S^1, S^2 and S^3 in Cubical Agda: > https://github.com/agda/cubical/blob/master/Cubical/HITs/Susp/Base.agda > > However, I don't think we can even write down the general version of > S^n as a type with a point and an n-loop with the schema implemented > in Cubical Agda. As far as I know no other schema for HITs support > this kind of types either. > > -- > Anders > > On Tue, Sep 17, 2019 at 9:56 PM Kristina Sojakova > wrote: > > > > Hello everybody, > > > > Is it worked out somewhere that the two definitions of Sn as a > > suspension on one hand and a HIT with a point and an n-loop on the othe= r > > hand are equivalent? This is also an exercise in the book. I know > > Favonia has some Agda code on spheres but I couldn't find this result i= n > > there. > > > > Thanks, > > > > Kristina > > > > > > -- > > You received this message because you are subscribed to the Google Grou= ps "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/ms= gid/HomotopyTypeTheory/6c150b9c-fba6-47c1-2a6d-975b90f64638%40gmail.com. > > -- > 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/CAMWCppm0sB2ZDMPM-jUYVpn8qxFJEfep6rsZs%3D8k%3Dhh6yGQF1= w%40mail.gmail.com. --=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/CAFJ3QW%2BznvLhFgBODptrjnKcY8QaEH8BxD3adrgRUNvo5fU%2BEQ%= 40mail.gmail.com.