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-pg1-x53a.google.com (mail-pg1-x53a.google.com [IPv6:2607:f8b0:4864:20::53a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 56f67c10 for ; Tue, 17 Sep 2019 19:56:33 +0000 (UTC) Received: by mail-pg1-x53a.google.com with SMTP id m17sf2653869pgh.21 for ; Tue, 17 Sep 2019 12:56:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568750191; cv=pass; d=google.com; s=arc-20160816; b=veMfyb7cBh/HPdMWrlvjBAWJzbEk1rRBGSINbswxsJjQQCeCAsJ4KoFpp5AoNZ1ola ARaa1MIJkLj2+cGKBKLBsafCFgheyRsPdgRQjuQIIcYPDtmx9gTuUecuLWFxzgFset6s 07GCbSrBvkRRPNffZHqYtcSfTGFcph1Qxn7OTiDyt7BnYEJnUF9oWAOCbAeulFALOa0g SD0zEbc9cydKgpuofHXxNXjvUjPCBfeOhUEDQ8QHjV++7MXLaWXnvmN00WPr7mMPDMk+ MqGK2glO6QTFocM8gO3GUvFXxw01xXym5lFePT0PTkOkbevvFTrUzEMqXIAQ/Nd04ogc ILtg== 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-language:mime-version:user-agent :date:message-id:subject:from:to:sender:dkim-signature :dkim-signature; bh=v1HM4UOl5lsKAIP9OKiSKsZi3cfEu8ZacJMxCXFNIrM=; b=dXr/VkFbZwrkP+fXWet+W9tkzifiQ7ml3ATfuNYJxQ1zeNIV9CK9pfwBNRCKzmPYYX YOIQhrDLiw39Ln2a4Z7U6XuSkgIJgrZa5Aa1GkRf555++LaYcNRZHhntyEszf6BEtRV5 OPTOeurkjPkKG8C8K5KpMPp5zkEhaAA4APKDhVwsrC3hvZzwcpf/QW5nP4inoWd3T1wf aTFABfiAGlFtsVK4rWBvvA7FwKBpNddoJhKLRumDylAiiaago6cAZy7U9hQp5PJGTLhb doyM3GMwYqFpcBJRLnOXEFzPThD1YpDXmqoLHB31c2rkjY3OwhEywJHdJDwBWY5FW4Fi SgfQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="j9Q/ve4v"; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2607:f8b0:4864:20::72c as permitted sender) smtp.mailfrom=sojakova.kristina@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:to:from:subject:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=v1HM4UOl5lsKAIP9OKiSKsZi3cfEu8ZacJMxCXFNIrM=; b=gmqaJSKX0IE1WDub1p2v2tKT/k80nIttYgnXv4uKEsBO/gep/us4yegqxsjaWrQGyg IgsDRrS/ND3QsFIpBaDvWpZO1lPg5X/nSvrjZmHEVHT3Hd3iDVoilJA+mMZ9DII9LVEA X6e7IOXGtfKAWY0sqiTQJFqcV/D/VtzpHZcPwNc8YhBmMevRFzIbScKSNCI9xeoUL6y4 sl+dXbfFcFj+li9X9MXUEUwfqnyOfFBcoyXZxHO9IALpH4vXv8ER09FLkm7vSRVudKKq 2t7x+Juwq0Or4jyBo4JYoON1GPrximXq5oW2znJeKHEowVDrdHSInGQlkm/UOCjgFXoR lIaA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=to:from:subject:message-id:date:user-agent:mime-version :content-language:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=v1HM4UOl5lsKAIP9OKiSKsZi3cfEu8ZacJMxCXFNIrM=; b=aBBD5OT02lPtRy+BW8DLwERTO+aMEaNiq+y6WY2I84NHf88eZfvg1Ix2rUYuI6eLYJ XFW4iXaPqrCY8USIPxuoP2MV+yWYmSTgCpJQ53dIiLD9KjDjsV3mogp3YDZcsdmBiuwX BkP1pmB55kjjPUqJfd2QG4g8DuhUyV9NAHpKgS44N2EzxsZBJ8zE7KlVRs0BZQdlRjAf 0+rLab2h3bN9fLiLUmurLVi/SCWNFf5ZCzUc3Rw4Q0en64PFFmmH9N9qOUDRdvdPZ3Mm 5WzpiuiHaP5QGYlMMais8PnLtoHJ0IFij2y5+3HDF5mWdKVUI8Q3um3pEqK030Fd1M1n 4v3A== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:to:from:subject:message-id:date :user-agent:mime-version:content-language: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=v1HM4UOl5lsKAIP9OKiSKsZi3cfEu8ZacJMxCXFNIrM=; b=CjoZ0mhvmv4CYQi+kFekCewZJbUs8ezcfE8xWIqkWxWnMLO3X348IFgA+HrKNZZfWE Saydmp6j1wPU5gfGlNwoL0/3LHOmAF/8/z1DxC4+FifyL5LVRIaKHTAuw9bSVonwCTK0 fLlOtjYS6xMDAvdfphE7CehZRuNP+XIg7Eh4g/bhbb8YLuRSch+b85myYpptSPPFHAje MK89RhQs+XLEq8QzUSdgfUEPBrZGSMNQ6HP659XtBcYTV1vdR44VVzg7NdAF0wMmVkeE ctACNIJgnAo8aGA/c+IPAbgkp2O3gUZs0qE76n2zQsSgwgKLBthXx/Y5R3GE+bPAhZzg 9Qkw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXFJkvC7daHDj2Jo/fi5Qbu7ycPO1XyGEhEt7uzfrjIPktiKqP+ 2Hpnp+I3ty9Fj11nTZg5ak4= X-Google-Smtp-Source: APXvYqw7FHgvNysALeubWMtuKLR9+N3iCUKDTpqm3gEJl+9DT70biQBWxDnelO4MAdnyPe2Lzpk/Fw== X-Received: by 2002:a65:638c:: with SMTP id h12mr536668pgv.436.1568750191518; Tue, 17 Sep 2019 12:56:31 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a62:2b90:: with SMTP id r138ls1094938pfr.7.gmail; Tue, 17 Sep 2019 12:56:31 -0700 (PDT) X-Received: by 2002:a63:1341:: with SMTP id 1mr585847pgt.48.1568750191110; Tue, 17 Sep 2019 12:56:31 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568750191; cv=none; d=google.com; s=arc-20160816; b=SqRTLMBwUvNP8m2ZMKUMpoePgRfoRx7d8JsYPPLf0UbNfln8LVQrXvByTlhSSZvVv2 nlPPeYe/l7q46dYRDcRliT/QT39WxqgRjDQdRnBim34JmQQDSdRqpLsQz3KlFUVaT8wo imEggEDQW1LnRcDLC0dnQKyV+mepUHNcWSRX7imXQwuC5ZftzvlsseG2Yhx2k8TufsXF Eb8+GzaBzC1QJeXguZ4DbsRq+xrbqoWuY65h1miFuKffbZi36RqkCpOeWZwi5FLyxsuu 10aXc6PNTcGsV7ySnsWPDDe5XWCYTGu2SnDNrgdAH0fV5w9DAxevSeeJIryE/P2U9tws yHag== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-language:content-transfer-encoding:mime-version:user-agent :date:message-id:subject:from:to:dkim-signature; bh=e8tFkCfEEaTHB6TJ4p0ZzlQPBRIh0qCvryghuOtwh3Q=; b=dbOBVucd3hjhHOCwVKq5IooCA2/tn5fLGDU9A97JXdZHSENyFJQqE3rObuKOCF7uNN kTdl3e4ZlD8hbHGJ2IPIwBQrWnwP75dOiTGN/izt6mVVORUM9wKInWXKush3K75IA28H Ue1TYyj82iUn5u5qEdAK7UUgibQEAFfy+mBjB2fp/2NgjUmeoSZRYDzfZOwm6KCUE+Rl 3snudRJvIZFKnKkZazxYhIpRNkSPEHbNPQT3z5O7ac2ygKk0D3kunsVLOaZ6/ubcdb7a 2T0vZVrTh6Js8KBf8JfBNu0XmCRO6ktRz49D8QF2gxjzMpjp5gYQx53ANh+WNr1kOQA6 aR4g== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="j9Q/ve4v"; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2607:f8b0:4864:20::72c as permitted sender) smtp.mailfrom=sojakova.kristina@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qk1-x72c.google.com (mail-qk1-x72c.google.com. [2607:f8b0:4864:20::72c]) by gmr-mx.google.com with ESMTPS id 85si468790pgb.2.2019.09.17.12.56.31 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Tue, 17 Sep 2019 12:56:31 -0700 (PDT) Received-SPF: pass (google.com: domain of sojakova.kristina@gmail.com designates 2607:f8b0:4864:20::72c as permitted sender) client-ip=2607:f8b0:4864:20::72c; Received: by mail-qk1-x72c.google.com with SMTP id u186so5390701qkc.5 for ; Tue, 17 Sep 2019 12:56:31 -0700 (PDT) X-Received: by 2002:a37:470f:: with SMTP id u15mr215947qka.290.1568750189137; Tue, 17 Sep 2019 12:56:29 -0700 (PDT) Received: from [192.168.1.136] (pool-71-105-69-112.nycmny.fios.verizon.net. [71.105.69.112]) by smtp.gmail.com with ESMTPSA id x76sm1677323qkb.29.2019.09.17.12.56.28 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Tue, 17 Sep 2019 12:56:28 -0700 (PDT) To: Homotopy Type Theory From: Kristina Sojakova Subject: [HoTT] Different definitions of Sn Message-ID: <6c150b9c-fba6-47c1-2a6d-975b90f64638@gmail.com> Date: Tue, 17 Sep 2019 15:56:28 -0400 User-Agent: Mozilla/5.0 (Windows NT 10.0; WOW64; rv:60.0) Gecko/20100101 Thunderbird/60.9.0 MIME-Version: 1.0 Content-Type: text/plain; charset="UTF-8"; format=flowed Content-Language: en-US X-Original-Sender: sojakova.kristina@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b="j9Q/ve4v"; spf=pass (google.com: domain of sojakova.kristina@gmail.com designates 2607:f8b0:4864:20::72c as permitted sender) smtp.mailfrom=sojakova.kristina@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: , 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.