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-oi1-x23a.google.com (mail-oi1-x23a.google.com [IPv6:2607:f8b0:4864:20::23a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e055127e for ; Wed, 18 Sep 2019 19:19:32 +0000 (UTC) Received: by mail-oi1-x23a.google.com with SMTP id u69sf615606oia.13 for ; Wed, 18 Sep 2019 12:19:31 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1568834370; cv=pass; d=google.com; s=arc-20160816; b=Lpcw6cg4cpNoK9fqiE5w+cFgjzHf/EBhxkZbDxVzglvSIWU6YD3qfORx0SNpQDbuJZ V2vFQHjQPz67EGXEksSFDLWVL8selj0G/Qg95TrDst1ihLWAGhBB/HjPsLbKmiN6KTJA JG4EbO858JHMDIfHa5X9zG7mD3cDaDGi4KlWTUIqmN7V4wf7iiekiXa2E0DuP3a3qAT/ OEmw8N1WRRKrlKhqtduDvZnoTPl+yEsz+letMY7BDT1/vdS4vdX2+yNPpm2AcMZEncEK iSut3FIwZ6x4hXV7qC6CB+Z6Gl4OZEvPlWk0mVZjTet5RppL0N6Gckg6I4EbEyHzSHZQ XObg== 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; bh=pa8KbXnCkf8EtVvr/A/7TSEaacOSvq25GBFdRBd9bO8=; b=ZSnDoGq1UnFu5iiLWOLlqlQHIP8IW41AeZVyHGP60Lkd+i3CeCt3RSmV5TG4RvQFFW sN6JHs1nqgxzB0mWCDfFgQUTLTKA21fqI5zjQGP8yWSkZvwNpjc8sHqjnFUmozW9+Wna lv+E1ySdwynAcoXKxoUy83zYapfD6fdP4ydkrxCo6/yUUantnaw/I+qlaG/6iwvHVZsr Lypd/SpuSI0q20aE73ksduR/xDn2l/bJF9kj8QToDALmRbz3vRJpYFclduSzfvfXO88O u0KoBTCepy72tSxduT5ezM49xrNm6nx/w6bYTM3EuR7iNQ2IRQHJ2VSGFceSHmyHiiJO ifTQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pd91f0Be; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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=pa8KbXnCkf8EtVvr/A/7TSEaacOSvq25GBFdRBd9bO8=; b=IvRPKjThHCPuE4JtxH4yV3QQGVDNnjqXlhLJrMqVPVT2Iw9MB+pi4odAx9zhf5J6mZ 7z2vufV8Tw9COkysXabn95YkVKNrx2LIC7B+w7xsCZ+e8pv6hOIqI5Ji1oGOWKkkn3XM 4dp7CLMXt6JtiQjv6GD+F1u8SXJhJVeoIvypfPKoJqHMuzkSSa2DFJJF56rnwspNdj7z vcq9pvoVDCgzBUVN5I9/8f8MCVJmvnI9afSCcBr9nbtHxWVtOjaShbRRE7z76drxRgqd CiEhYeM4I2S4Q8KrYgVxXKgxWr3jzZ/Fx/aRfqgaiUhpdFXQAPApmwRQs4pkeLbEtztZ o4Ag== 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=pa8KbXnCkf8EtVvr/A/7TSEaacOSvq25GBFdRBd9bO8=; b=Uor/w0qpt363uV5tivuoXEiUiyENZR5IMtrPYzEfU1ukoPy52Bxi1fftNblh7HT5Fa dGJr2gm90OyHI0+FuiPdIZ4hxNJydwAB7oZKrh3RrYhHgTUfFSTeUlQTMt9/z2bz1I3L dEAQ/yT7mdN+YiMkN+SvFXZxfxcji08B/tIMEou7FSpD/7GQFskLWdUktmMSWTOjMeVg 2Mto8ej3QakadjQT1RCmuSb0spL//et+iVQ+A1SYSMOMfTfCeOzZbqhkrLJJTgM2d9/P fLlPF5vwK4JBywpbe4KnhEKuj4VotmHBES6g7ZjOMwsU3wj0DQXI37LIa1MH5j0IhUv8 s3vQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAX9miFC5A9eUFE5r8XVrx9QFQT53BqDAFNQwQxyGZqqnCRPkWzb oYGKWWZ8ncORaAiusqBAn6E= X-Google-Smtp-Source: APXvYqw8g6Zol0S4bvCjwEgp/oF2X6hZWOA2BCXBzxaRMz9Peh5byA+tVKRNEyShGwTVchR1mvb4Cg== X-Received: by 2002:a05:6808:8e9:: with SMTP id d9mr2420477oic.24.1568834370518; Wed, 18 Sep 2019 12:19:30 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:4fcd:: with SMTP id d196ls119577oib.16.gmail; Wed, 18 Sep 2019 12:19:30 -0700 (PDT) X-Received: by 2002:aca:ed0a:: with SMTP id l10mr3566726oih.83.1568834370187; Wed, 18 Sep 2019 12:19:30 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1568834370; cv=none; d=google.com; s=arc-20160816; b=g52TvEUtoZmghXlSQWIJkF4wK/GMM9PfZd1l0lFMslsXHWrD7fAfAHkA5bJcKh4kS2 e3HuFBA+wesS0z2G6HpEy5AuI+CgMprEAQIKG7yFaEDwBdHQeMVptjXatMwNPPZE0Tu4 IaASqGFK6xZxxqWLH0ULsJG+yMMfUEkMxfl7lHjz7nGF+cGU3o6gxwCwoj7yR1Q56Y8A kT20P9K+ydtygkaFAUXyfKji8Y0BJt5rAQC9P5SP+kxF06r/igf3roC1/XwkHGIqJxAD aQV4DKJRNuk4moZu1hYrjrlVjPp5+RxbZbMDGoZsabj26OMux4baj1RnbB5BoHDohMhg Xm/g== 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=2q+kxs7AwJ/bJ/bp1JjSnOu8bTj4XPoF+AN/5K4pZ1E=; b=bqPLWlaXzmrJvZ7X/jvBqdl/U+q8WEpedqFSZWN1JWXd/522OWCQRf919ApKqeVgep UOT/x0qxJ4EE+BVobh05vLV9syPmbPLzriznSx57iUTmv3A1IaMH3xavbo4HRzqiiEcC +HbRmUBo4/FfT4aG4VSmugqYbAlHJV1P6O3VJs6Bd+sMVSnqsikqilGLM+Ra54nJskTj uul+O5P+w4JRPB+yHv3Cnx4s1AW0spfa1cVK4MYtFYnHGt/1d0o9s6kXDJIQNM9F0CjN wPWDrelQTxQGh7MJZQoBMOM4LOeki59MImb6/liN12K5xbzm3TMVqd9ZnX4Isv8kFCqQ VIWQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pd91f0Be; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw1-xc34.google.com (mail-yw1-xc34.google.com. [2607:f8b0:4864:20::c34]) by gmr-mx.google.com with ESMTPS id a22si334935otf.3.2019.09.18.12.19.30 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 18 Sep 2019 12:19:30 -0700 (PDT) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) client-ip=2607:f8b0:4864:20::c34; Received: by mail-yw1-xc34.google.com with SMTP id q7so352955ywe.10 for ; Wed, 18 Sep 2019 12:19:30 -0700 (PDT) X-Received: by 2002:a0d:df46:: with SMTP id i67mr4366200ywe.76.1568834369726; Wed, 18 Sep 2019 12:19:29 -0700 (PDT) Received: from mail-yb1-f181.google.com (mail-yb1-f181.google.com. [209.85.219.181]) by smtp.gmail.com with ESMTPSA id k6sm1405972ywh.60.2019.09.18.12.19.28 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 18 Sep 2019 12:19:28 -0700 (PDT) Received: by mail-yb1-f181.google.com with SMTP id t2so403567ybo.13 for ; Wed, 18 Sep 2019 12:19:28 -0700 (PDT) X-Received: by 2002:a25:d1d8:: with SMTP id i207mr1144878ybg.182.1568834368277; Wed, 18 Sep 2019 12:19:28 -0700 (PDT) MIME-Version: 1.0 References: <6c150b9c-fba6-47c1-2a6d-975b90f64638@gmail.com> In-Reply-To: From: Michael Shulman Date: Wed, 18 Sep 2019 12:19:16 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] Different definitions of Sn To: "Licata, Dan" Cc: =?UTF-8?Q?Anders_M=C3=B6rtberg?= , Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=pd91f0Be; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::c34 as permitted sender) smtp.mailfrom=shulman@sandiego.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: , What I find more interesting is that it's even *possible* to parametrize a definition of S^n with one n-loop by an internal n. It would be intriguing to try to find a schema or semantics for HITs that allow paths of arbitrary internally-specified dimensions, and see whether there are other examples that are more useful. The only other vaguely similar example that I know of is mentioned at the end of https://homotopytypetheory.org/2014/11/02/universal-properties-without-func= tion-extensionality/ (and implemented in the HoTT/Coq library), a definition of localization that works in the absence of funext. On Wed, Sep 18, 2019 at 9:27 AM Licata, Dan wrote: > > Thanks Anders. To be clear, I don=E2=80=99t think we have any schemas or= semantics of HITs that accept this definition of S^n (with an n-loop for a= n 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 d= efinitional equalities you get) as implementing the one-n-loop rules in ter= ms of suspensions, so that would be one way to justify these rules. > > Also, the proof of pi_n(S^n) =3D Z that Guillaume mentioned, which predat= ed Freudenthal, is a lot more work than the one that you get from Freudenth= al, 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= . > > -Dan > > > On Sep 18, 2019, at 8:00 AM, Anders M=C3=B6rtberg wrote: > > > > Let me elaborate a bit on my answer. One might naively try to copy Dan = and Guillaume's definition and write the following in Cubical Agda: > > > > > > 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) > > > > itOmega : =E2=84=95 =E2=86=92 (A : Type=E2=82=80) =E2=86=92 A =E2=86=92= Type=E2=82=80 > > itOmega zero A a =3D Omega A a > > itOmega (suc n) A a =3D itOmega n (Omega A a) refl > > > > data Sn (n : =E2=84=95) : Type=E2=82=80 where > > base : Sn n > > surf : itOmega n (Sn n) base > > > > > > 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 > > > > > > data S=C2=B3 : Type=E2=82=80 where > > base : S=C2=B3 > > surf : Path (Path (base =E2=89=A1 base) refl refl) refl refl > > > > > > But what is happening under the hood is that surf is a constructor taki= ng i, j, and k in the interval and returning an element of S^3 with boundar= y "base" whenever i, j and k are 0 or 1. In cubicaltt we can write this HIT= in the following way: > > > > > > data S3 =3D base > > | surf [ (i=3D0) -> base > > , (i=3D1) -> base > > , (j=3D0) -> base > > , (j=3D1) -> base > > , (k=3D0) -> base > > , (k=3D1) -> base ] > > > > > > 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 boun= dary of the n-cell. This is what that is not supported by any of the cubica= l schemas for HITs. > > > > -- > > Anders > > > > On Wednesday, September 18, 2019 at 11:00:22 AM UTC+2, Guillaume Bruner= ie wrote: > > 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 a= nd can > > presumably be formalized in Agda) but I don=E2=80=99t think we actually= proved > > 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.ag= da > > > > > > 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 resu= lt in > > > > 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/db712ad2-396f-4328-bb73-898dcb956834%40googlegroups.= 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/DBF368F2-295C-4175-93F2-1EA01D49B95D%40wesleyan.edu. --=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/CAOvivQy%2BUGKt3q8P8ed9N6E%2BjOUcjgQ49pxp0rBuDM%3DSoV-Qb= Q%40mail.gmail.com.