From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORBVHPY7NAKGQEO3AT7HA@googlegroups.com X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-0.8 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, HEADER_FROM_DIFFERENT_DOMAINS,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE, T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-yb0-x23c.google.com (mail-yb0-x23c.google.com [IPv6:2607:f8b0:4002:c09::23c]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 45a1391f for ; Fri, 20 Jul 2018 14:55:18 +0000 (UTC) Received: by mail-yb0-x23c.google.com with SMTP id n7-v6sf6177436ybo.1 for ; Fri, 20 Jul 2018 07:55:18 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532098517; cv=pass; d=google.com; s=arc-20160816; b=DciWt7521dSHHxIZSJDR5UEhQYrxw1/5sGaRsmd8j67HTTZsl2kDW8kr40t4//gfew SXjeY+0cNJhsT1uUyuIF4DJyoe5kg6KwsBydg2qce6VxgrkmANOYAcc24eocuDX9zjk4 e2s13kZWBdMAtkRn+TjelPe+qfIW9hlghU1E0cPLdwWqojUXrCByZv2w25Q+3zjiMHw+ 9TckQVyW83KzC6u4/27nyKnINriVAGl4nN+tOnaAw1ekUQfMFfyPhcbZ8tUuFmmD/5or xuI6DpZKgvgZUkCuTlMMJcieE5m4u5QkCghcQ0utbaSBK9Rf2s++JC0dfX1/N4MMwFat TV7Q== 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 :references:in-reply-to:mime-version:arc-authentication-results :arc-message-signature:sender:dkim-signature :arc-authentication-results; bh=8q5a75LXEgxWlpgUIFDmrLGrDecfsXif2dZ6d6GjWaA=; b=fV8mjuJsXo7uZ7Jb/sjRfr1T47zPjpztnShCdnqzWWLNIw3UbgC5bqElxiqfG4k6OO vE5Rwlpe8OUHrkb0zuy2zN7PgaZ4GYyDkniyTFmbRmB/+pNcHcWNeKjjix3amZDM3R3J hbpYx3pUzJkHxRJJOiSXspC7GkRDyYkdoiWOcpzCCNl3CocQNAFQPZCqwV3u8IhUc13c qAVF2Llmv18pBH04VEpADI5zO9YH/uzqgtKu3lTPggvcJUoO9mt84SVmLpe+gStHEWcZ IxTzL9OGDBZCVh0d+lGYLbGD8Z6nwWmA3O99kORC10RqLvE2gYMSuG0SZSnu2STuxCsB nmjw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=o6JCU7W2; spf=neutral (google.com: 2607:f8b0:4002:c05::229 is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:mime-version:in-reply-to:references: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=8q5a75LXEgxWlpgUIFDmrLGrDecfsXif2dZ6d6GjWaA=; b=Bg46CMKksI0RzcewdMdYOUs2LGEY9XYGagtNCTjiTy6NAISNfoJfGXzQoQMxtwqOOZ jUJrbO6CgG7GHVLIPZo/3f3qpTjeltMUo9/9FsMEvaEqFuYbHJOFJkxWqco4eEFMhkRG bW0a6kyiAaGy+2gB7b57U6g3y6PuPeW1WxsDlpaaNaFSGMnGFSef3V1K0sBPS2GPLFV0 Bf1R5enrqZ8tFJjmIT/JP2E9nsZO1THk91BGBc61S4riaAYVHakW1KsfyLFT/LbrgtOS otZEXfcZKHY1gKVxHl99GF0d1/zaQaVB+XUgORTNiOSw0ar+bEl+ZwruQpOYQsldZfjD 7wOA== 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:in-reply-to:references: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=8q5a75LXEgxWlpgUIFDmrLGrDecfsXif2dZ6d6GjWaA=; b=KWYGarAxPQN+SQViD6R32SeIOKi5wQ/oexC1XLiYu0zbM/EWyqZZjGOtW1ebfkeDOr qUaqSGd2QPH8EetNG4t9URj0BCaIF29aaJpukuZ+KdH4hLGdVES1VGK1VFLc9+H0w1WQ qfwciDuGS9Jp3gLXaiO+SOgZBPd4PLH1g0XGPbP//rrrfVpekJZeeB17Typk+j4tLUfY g+aVp4hmPVmVC1nwntdcSXlq8vYnkpYXTCV6OWxZKNIRf3CYyO2bzoVatWIbQy1eKlKg Jh9t+hl0QottmaBvku7AoiGd1CZL4ZeRdBfIm7XDXcNDLd0VQ2xPfy/X9Ogz8mMuQxLv zluA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFaDMG1soOE2yZPgDZv3oeMJFtGw8tP4wIy4GfdqJmMaNBPREiS tj3U4zHuLrhXtolqAgMU8ro= X-Google-Smtp-Source: AAOMgpcT/Tw9o44wXdvBYYtcMDovbR9Us1jv0sTH6Pb6A4qtZ6C+FJL+zQOKDGolSOYQnThPA2V4zg== X-Received: by 2002:a81:7dd6:: with SMTP id y205-v6mr64561ywc.1.1532098517053; Fri, 20 Jul 2018 07:55:17 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a81:ec3:: with SMTP id 186-v6ls327377ywo.33.gmail; Fri, 20 Jul 2018 07:55:16 -0700 (PDT) X-Received: by 2002:a81:5295:: with SMTP id g143-v6mr676799ywb.142.1532098516711; Fri, 20 Jul 2018 07:55:16 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532098516; cv=none; d=google.com; s=arc-20160816; b=hbzz7DnKePMiXez52y9AaQ/ztlQL91pz4NzkMxHuBH76jFK3XbRtZ8OOuEbE4w8LKW 6/F5mQg/rAk1edw8GgitJzjACgPbh3OVRDzAZYxCJFA89UTwfm+WjUbE5ILpfMxoA+6W nUfhF2WZWm0rMT8UoK+Fe00nvqmWztdLiEOayB0N+FvQqvz05wcEYp0XqwtOTUus1X7O e9tOjM7Emoy+fA/oQnqKUFWpHftMCVUAD2mC5kkj5JVx38RcqeeyRPTx3dNil7SJJOTV ZKJj+Tt/uYUae2j7atwFsVpQKHINwEysWuvP7wtapD5bXiXOJPmjrNESQWVHMMsGxubT hebA== 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:references:in-reply-to :mime-version:dkim-signature:arc-authentication-results; bh=YF/oZrgSeNegovqGz+zS7JfpLFpSLTXfreSiqnYRS1I=; b=DHJIfBVB4LDr5uJV6kBMaHbW6NkQR6+EM+mwWdArphtxqD6Xz+AyUpL5ggJ0d3/GXT 4QwhyKIaVXm/tY6mDOhCEeElJsrbVWanAofKv1FWRuEWsw/+Jx8hAg4M1LBhbrsH6pfK 5tY6gUgcompo73qwhTECTELn8UkhUQbj3dGUDh8StQ+nj99t7OSCa33i8E2EyQMmMqKV sYfg6RiUoRq03zuvp1VDwTSHQ6HujgzcECZx4OUpsB8FgwCGpJmtAl+UInlirhtDylak lNxLJGrrMPqq8MlrXK4wdnI+hA2IQZfBO4SFvhK/OT5rd8SUcHzWoItVpISYWebQhi93 Ak0A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=o6JCU7W2; spf=neutral (google.com: 2607:f8b0:4002:c05::229 is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw0-x229.google.com (mail-yw0-x229.google.com. [2607:f8b0:4002:c05::229]) by gmr-mx.google.com with ESMTPS id k66-v6si141797ywg.0.2018.07.20.07.55.16 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Jul 2018 07:55:16 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::229 is neither permitted nor denied by domain of shulman@sandiego.edu) client-ip=2607:f8b0:4002:c05::229; Received: by mail-yw0-x229.google.com with SMTP id r184-v6so4443315ywg.6 for ; Fri, 20 Jul 2018 07:55:16 -0700 (PDT) X-Received: by 2002:a81:e301:: with SMTP id q1-v6mr1193828ywl.499.1532098516350; Fri, 20 Jul 2018 07:55:16 -0700 (PDT) Received: from mail-yw0-f177.google.com (mail-yw0-f177.google.com. [209.85.161.177]) by smtp.gmail.com with ESMTPSA id j4-v6sm873225ywe.36.2018.07.20.07.55.15 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Jul 2018 07:55:15 -0700 (PDT) Received: by mail-yw0-f177.google.com with SMTP id p129-v6so4442389ywg.7 for ; Fri, 20 Jul 2018 07:55:15 -0700 (PDT) X-Received: by 2002:a81:6588:: with SMTP id z130-v6mr1178974ywb.155.1532098514989; Fri, 20 Jul 2018 07:55:14 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:4094:0:0:0:0:0 with HTTP; Fri, 20 Jul 2018 07:54:54 -0700 (PDT) In-Reply-To: References: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> From: Michael Shulman Date: Fri, 20 Jul 2018 07:54:54 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] What is knot in HOTT? To: Urs Schreiber Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" 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=o6JCU7W2; spf=neutral (google.com: 2607:f8b0:4002:c05::229 is neither permitted nor denied by domain of shulman@sandiego.edu) 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: , It seems to me that especially if we want to construct *particular* knots, we would need the smooth reals to at least be a ring and probably to support trigonometric functions. On Fri, Jul 20, 2018 at 6:45 AM, 'Urs Schreiber' via Homotopy Type Theory wrote: >> Once we have the "smooth real numbers", wouldn't we just define S^1 >> and S^3 in terms of them as usual? Or are you saying that the problem >> is in characterizing the smooth reals inside differential cohesion? > > Yes. > > Possibly one could make progress by declaring shape to be homotopy > localization at some type A^1 of which we only demand that it be > homogeneous (as in Def. 4.8 in arxiv.org/abs/1806.05966) and then > focus attention on A^n-manifolds (as in Def. 7.1). > > One could maybe declare that a smooth n-sphere to be an A^n-manifold > whose shape is equivalent to Disc(S^n). Classically, this should work > away from dimensions in which there are exotic spheres, hence in > particular for the case n <= 3 of relevance in knot theory. > > Best wishes, > urs > > -- > 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. > For more options, visit https://groups.google.com/d/optout. -- 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. For more options, visit https://groups.google.com/d/optout.