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-pf1-x437.google.com (mail-pf1-x437.google.com [IPv6:2607:f8b0:4864:20::437]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8d99cca3 for ; Wed, 18 Sep 2019 08:32:33 +0000 (UTC) Received: by mail-pf1-x437.google.com with SMTP id v3sf4373817pff.4 for ; Wed, 18 Sep 2019 01:32:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568795552; cv=pass; d=google.com; s=arc-20160816; b=gZzhGKKXmM1tz14yGxKdTFFb+H9lcow5/u1OGBQ7Dc0PE6kH2Tc2pNG7z1l09Fl9t2 nAgLYYEdJenRI5F4at1gdWlwJCxFSTBFNGKWvImOmhQuepwvJejsj00KnnyAT6eyJl/s f/svtNP3MnUx73/McJVM/vSz4xb8xrmqBXCZMHuJ0g7gOzWuJw/5qahyOSHG9hcG4Byh unB25XHIlGshiYf+A+zmix1hTJuo3ZvdjXrpznwsLflLR47eu8MfQt5qzM4cU5IWJPg8 Y80s+Kg9I0CbRpoJjUtZ9Ziwtr2ARSghEfMU6dbAlivekxnsfx2UYscy25rDSxGVTP3p yqvQ== 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:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:sender:dkim-signature :dkim-signature; bh=+rgyw5o9pfuBauHxykJqOinSj/Ws/xOn8xkXam3TztY=; b=M8lvxclPZKqRFjZboPS2ExpxSVjzNLoEBOfxrDAZo7eVaCIp521ib7lbPgP7+jJA9j kXB7LdllauDKjuDuSFkDBPo54GTkiWkz+Ayyfun6uGQCQu37slYbLJnHb+t+7PJuL5aI zoFv8UeuS3UFi0ophtmty+0bU4YEvc58T4gY8xNE3YNhTHqn7/lDPkJaoDimV6yAyAgg vFE7i1IGgFdIeCqgBiigvtN2+44fKKzvfeVJsz33mYJgbwIesAQhLBDMJbLhC5hkGHWk 76K3VTvTAxqHmnPc9IbDr9a3DqobUL6w5a60boK7s/MLITdjSbpJ5/0x5WrOL8VZIXHU Qm2A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=qqo+ZLHF; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::330 as permitted sender) smtp.mailfrom=andersmortberg@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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+rgyw5o9pfuBauHxykJqOinSj/Ws/xOn8xkXam3TztY=; b=LXT0F43+fe5tTNbkJ4kUBrl7yxiq211hq1elQLOCXEJVwKJDl4JgV2ixnOc69aWwtb kHmxFwbpxElqOm+1Ivw6tI3psVAb9dS/vJysuY8SiILQFcEmzNMURTB/eQA255sKWH1o MCxMlFWIaE6s97//U/Gy/rl8LPz/TObro5qkyVGXdG3jhSVfzkFHkzfjU+hjpKgKtnmx 5J9osRLcy3TdopqCe6ulqDfdC75ujQGj+QfrgsF916eA5qD80bU1xeOaOFXb0GYNKvCa nr6wD35Qd0DCKjVM/7ghUdERHbyWCiLzNJw30cxHzAyoKd60VSOqq10Jj+uDcwq+BCbP NPXQ== 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:x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+rgyw5o9pfuBauHxykJqOinSj/Ws/xOn8xkXam3TztY=; b=A+/4mQgIPxWnIxJ3Ov1vW+sir0fZhMA0Mave14jsduZtCt7gNobxqRWmVUdt24px6i 1ZZtbhalIeWtdXy0GMRL4Vj34stTyJoU40m8R0iY6/JDo5P7Lfu2/BZnmBBN4hyLCTzK d0pO63LkjeWe+gukGasTPz0qU3SAlexv0TtI7w5LK0ubJu8PzD5kb3Q7GtSAc0cOouzo zi04Yv3edqtNxJS2elQCNVTWtNo6NtTBMO/ZZzIuivULpInr3CP/7nIjCKv1fO0AShbK 1tIAD+lA5bVeuvA/3Q7+Pkl36TBQB5GtWJUrn0w3mHDlHBzvHJUg96mBpwfirVtFmOY3 /7Ag== 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: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=+rgyw5o9pfuBauHxykJqOinSj/Ws/xOn8xkXam3TztY=; b=bWbHMjHDdVDHq12/HNrVv8UjjtgG0G1yH1LZG2FMm9CsxAkDNPUHGG8v45dFfyjXx+ UKPwiij9hhEYP9iK3kDsbmraJYVP3tnIQFcgAiJ4bDLO5ny8cuQVn7VnH16RYkfPku25 imTTADIPc/dWXLJhRsTEn362uD2m4HUOahqxIckqBZXnhZeUuKZbr/mbms+ZRqmLdEzl 79kzP71SOpX84xtTKNrhOoAkfQcJH0XADL9dahqGLpksj/0cZiISFv0icrOjz0dgHjD5 5Sg9pD7pKbwjf6Zr4t4zM2okCBX9xt1+LaHN3i+Q51I7masNqRDf/dmhwVTfI3p2PvaR A51g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAW9fk/1nEdHWOe1EF2WiIppKfXgLTSBIU+FfXNm+ahcM89TKzzy wHrX3AbJ+4CNNn9xoqIMAR4= X-Google-Smtp-Source: APXvYqzC5Nj6zDg8klm3gVE+j7AJpxZv7v3DSkKehdHa459ZYoBkNHltNubGu1DC8vY5CsapkZhf5w== X-Received: by 2002:a17:902:6b04:: with SMTP id o4mr3059330plk.278.1568795551763; Wed, 18 Sep 2019 01:32:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a63:3043:: with SMTP id w64ls1326409pgw.15.gmail; Wed, 18 Sep 2019 01:32:31 -0700 (PDT) X-Received: by 2002:a63:c442:: with SMTP id m2mr2909863pgg.286.1568795551346; Wed, 18 Sep 2019 01:32:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568795551; cv=none; d=google.com; s=arc-20160816; b=fgPaaavRJMUtuZ/R42wF2gQEDwXKnIrdHlPK7Z04TdLAETSAoTaTZuzwFSVsZz01w/ SlA62uYMlEmh0brr3gQxqpUu76619E+ZGb256/7aRNnKtCRyuK32FrCbvgIH3r3231S6 DuBXW+G+DmDl6ihoMyqUrW8a8KL4oR1STJT8a1STtlUpHMBkoYqeQ/2OCuCHJDMCELUP LCq3feUxjLEzsQ6f8KlPCeG4RIF/Wqpxvur01GIp0rYGs9ZJeSLWOAF5pjV3Upm5d036 EzPSDqHyi5XTj0JkZnSImSgN9JnHoLRJl+JpDubGwzxUJJC/cyBLXFDboQnI6Il8xSRY dOdw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:dkim-signature; bh=5b0uMsHle1Yjv1pxWq9QuUshGmvWCkGyYZjp3LnA05M=; b=FegG2Io8Bz5jNUpJdKgExfF6YctR9AVPPYISXHH/48GbWTdFiQQIT4jjjeqFbZZutw ktCnmLTZWlkNunOlgTBmgDsAyToA2sHEvccd3Z886H/AvJT8U4ejyhlSucM6+l5unMuy UfRPz/+khdfyrguXHSSBurqJ8kYJfbzYeXx8WSl9A65VOfQJBtvueFKHsCEx5Jwo7jG7 xJIWVY4SEF/ML3dhrJALQzjZpggzaHXSouzEbdMd9YPT+qVkMRQzhXnWRSKQGMx9XYlR yvR4TAvbTRmqSvYphd9UtFJfhJPlcMRb5QbdNqIubMavOH7YgtZBQrCEuqdxhMlHaY6U veTA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=qqo+ZLHF; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::330 as permitted sender) smtp.mailfrom=andersmortberg@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-ot1-x330.google.com (mail-ot1-x330.google.com. [2607:f8b0:4864:20::330]) by gmr-mx.google.com with ESMTPS id d8si74308pjv.1.2019.09.18.01.32.31 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 18 Sep 2019 01:32:31 -0700 (PDT) Received-SPF: pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::330 as permitted sender) client-ip=2607:f8b0:4864:20::330; Received: by mail-ot1-x330.google.com with SMTP id 41so5538357oti.12 for ; Wed, 18 Sep 2019 01:32:31 -0700 (PDT) X-Received: by 2002:a05:6830:11c9:: with SMTP id v9mr2073831otq.125.1568795550913; Wed, 18 Sep 2019 01:32:30 -0700 (PDT) MIME-Version: 1.0 References: <6c150b9c-fba6-47c1-2a6d-975b90f64638@gmail.com> In-Reply-To: <6c150b9c-fba6-47c1-2a6d-975b90f64638@gmail.com> From: Anders Mortberg Date: Wed, 18 Sep 2019 10:32:19 +0200 Message-ID: Subject: Re: [HoTT] Different definitions of Sn To: Kristina Sojakova Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: andersmortberg@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=qqo+ZLHF; spf=pass (google.com: domain of andersmortberg@gmail.com designates 2607:f8b0:4864:20::330 as permitted sender) smtp.mailfrom=andersmortberg@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 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 other > 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 in > there. > > Thanks, > > Kristina > > > -- > You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. > To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. > To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/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/msgid/HomotopyTypeTheory/CAMWCppm0sB2ZDMPM-jUYVpn8qxFJEfep6rsZs%3D8k%3Dhh6yGQF1w%40mail.gmail.com.