From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORB6W5YLNAKGQE6RTTZCI@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-ua0-x237.google.com (mail-ua0-x237.google.com [IPv6:2607:f8b0:400c:c08::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 362358c1 for ; Thu, 19 Jul 2018 15:32:12 +0000 (UTC) Received: by mail-ua0-x237.google.com with SMTP id g19-v6sf730608uan.14 for ; Thu, 19 Jul 2018 08:32:11 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532014330; cv=pass; d=google.com; s=arc-20160816; b=gcmmXgOynnYX+1/terQIvn/AZclUzvrDGISMXKcQQ5O5FDGLjRrFNDHKXbTI2T0eI9 rhe3d68n5kZu7P1MsX8UlpCjcg4TX0WQnp/h+VJWIACzgQfS6MLgWQsKvBhLlAPu3XSb O38qI5d03t2YbHdiQQbTvBXSyTqyCW7wrQ7sR8bejtx+cjQqlDbhQwgebhzf8v8FajIj rNbZb4PWtGkvF5lgeF+OsRHHpIBU8vUsT2BP+5ITFEH3F+TRr7K8mjYC5sGmhdWTsKmk BbnpbN3Ju97T43Wy2fZVe9mbDX9U1t6c6KNjpTu2H/rDFC3kNiZUr4zH709IUfgmkP/w q2Aw== 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=4cse1QHXU8c+oM397Ie+QDUpzIOQNC1tYzT1VdeoLM0=; b=lCiMUBKk3q498liRKLfW/3QSqI8dQ2TdauDo1oKgdnRIF+jua2STffyU2aOVQMIfO8 MSrQPsYsZuvxs3i9A/2ybBD/yRMG3AetBkRbpZGNXG7LHW1+gEntr/K/5foJa9z9Lh0d BXoek1nPquNF9X/P90VS9GMeyF7ghEF51VnqQ8r1TExBkcuPcRNZF+h0LT2s0ZlyZx7P kS0Kg8Q889YeABdIo0LLgQYRFWdfAQCZfEhkmX9yrhX4xJ0oTn0MZhl/02a7FXzFwzqh 3eLXLpX20wOwqz6ZJ2oyQw8Zq2NTb332mj9VtK2Gxy+i7LQwSo2XE+671TUo/2AW2v3c h37A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=BoEvrHi4; spf=neutral (google.com: 2607:f8b0:4002:c05::233 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=4cse1QHXU8c+oM397Ie+QDUpzIOQNC1tYzT1VdeoLM0=; b=TSv8T/GXRYc6KjsgFfEdppRljvYnl2Ck6qYMggP1pqcusmEoUSwMBCgvvCZlVr96mN jS7T02MYqKngraRq5rV0lByd+Z6zHMyABt/eJnwLoT9mOJ2di8WfEr1o8hYT4K2Wnmos EuBZiiplR5pdKh2fn8tH4dpCaYsy1e3mOCVjM76C0eH3iuRZzgdmMIIiRGDvt7Gf5o78 VPx/jSJLygKn3TrCqpTQPo85f1q1KIpqZnpbUMmCAJVM/yRe6ulmjoO6v1wheUKASuxu mNaigj71nZrkFL/QHSh1pWngKmx+2xmiI/BfF8IhpWYYd5XeHNVWDPdnKHNeW0faIkSK uQOg== 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=4cse1QHXU8c+oM397Ie+QDUpzIOQNC1tYzT1VdeoLM0=; b=bSr3wkKlLv41jpax/5I67KZQWWP47E4nRkwaGQwY1DRYIWrxz7fUQKI+1cBMaCd13n wvJOZgcFhTa3ibI6Kl6W1HI5HpHsc97/YJNUNqSB5/w0nRrs6zx5RY6BvRaSGBGTSMHQ az7/d3LER1weghpzV+lH5akZYb6CnV/TAG7UqpMqDhzSGNabBGAXxn+xdOBdHwoCdaOR PHWRaegJIfODIfo/GtYefUbrlnhPR98qRMKUZ9FaUbV22K+XSeT5MeZK0cF+rp92J8eE KUU0Y3u9Q16Gk1kZ8Rcv+6CUhNFly3lWK2HhFK4cCcZMWP3gP+xSXnew7JGi1r+6XyfO EGXg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFOhpzr5SlapvpNOSbfMredkEBigg9VzIt1PypvTFWi/OrLGYFZ yl4BS2OIjIVZ9it6gKu8bVI= X-Google-Smtp-Source: AAOMgpfwKtnoioDyZGzXD376GHM/tlCCTRsw3+o4hkG0YxzKLKSVjVlibX1h2NOsao+uiUAfQ0jEIw== X-Received: by 2002:a1f:a548:: with SMTP id o69-v6mr51885vke.0.1532014330563; Thu, 19 Jul 2018 08:32:10 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:3806:: with SMTP id f6-v6ls501763vka.5.gmail; Thu, 19 Jul 2018 08:32:10 -0700 (PDT) X-Received: by 2002:a1f:b10c:: with SMTP id a12-v6mr4654902vkf.112.1532014330236; Thu, 19 Jul 2018 08:32:10 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532014330; cv=none; d=google.com; s=arc-20160816; b=PLUUYX4qXa+69hdziswugIl9lHk5FHGQJH3npjl7IHC9q8SJOZBkV5crlgSeoJtTjA Afy5rI9lIyBwHdkFjmntbIsxxScyZk6FkP1mSM2HZc7deIgs18XDjGB79UZR98eWQ6AG z+IgTbZXGr09tx20i6yUCj++ohiUF/zNUygeMQjjr1lDQDeRgj23jgKGVSUj9gYi4iMW 8WObTRBH7MFqrkQCzMaIuuMvNjzx0INce4disaEBv0cnk25uPyzgnycx/3bGbjwhl0EV reJALu4e5kC+qYkKUEq/QzOqfUJZT1UpI0GVaAycVrbScraGN8oQ29gqi3czcWz5Yaoo EG4g== 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=F/e1gftUCPk1yI88Z2SJVTFeEm9hXwmlZTHiDvWxQ/8=; b=ubroOeEd8RjFusYqBteh/J9i6iUjCSfC+fQEg7UMqiK+faPo834GKo5jSEeraxat4o YGxMhXhEOtV1W3WmkiR19DcrhHcgZQXk8+aERFBMe4cNXywS2Z7BG8F91Do8+1mPLqIf cxdAEdLuOtiZ9HwRUktDoL6ZLY8mUMaRU+mwRr2BP4LiVpRRh8JiJK2Cxlvl8htvjxc/ HNX2ie8ZA0kEzvOTanozIW/WIBxlBUM/qUXGMIpYzH6tofQtdIQfrsZUyQrw71eZsE8x 5i35qg0N7JuT/NbVHMIMUroASisYzY3gVMSUcbJ0ia56yQg0Y7RwAsS1lwuArfnvqGqB 72Og== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=BoEvrHi4; spf=neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw0-x233.google.com (mail-yw0-x233.google.com. [2607:f8b0:4002:c05::233]) by gmr-mx.google.com with ESMTPS id j14-v6si323914uap.0.2018.07.19.08.32.10 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Jul 2018 08:32:10 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::233 is neither permitted nor denied by domain of shulman@sandiego.edu) client-ip=2607:f8b0:4002:c05::233; Received: by mail-yw0-x233.google.com with SMTP id v197-v6so3217134ywg.3 for ; Thu, 19 Jul 2018 08:32:10 -0700 (PDT) X-Received: by 2002:a81:6f06:: with SMTP id k6-v6mr5390654ywc.170.1532014329686; Thu, 19 Jul 2018 08:32:09 -0700 (PDT) Received: from mail-yb0-f175.google.com (mail-yb0-f175.google.com. [209.85.213.175]) by smtp.gmail.com with ESMTPSA id a2-v6sm3569680ywm.7.2018.07.19.08.32.08 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Jul 2018 08:32:08 -0700 (PDT) Received: by mail-yb0-f175.google.com with SMTP id k124-v6so3414485ybk.6 for ; Thu, 19 Jul 2018 08:32:08 -0700 (PDT) X-Received: by 2002:a25:8384:: with SMTP id t4-v6mr5687648ybk.71.1532014328508; Thu, 19 Jul 2018 08:32:08 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:4094:0:0:0:0:0 with HTTP; Thu, 19 Jul 2018 08:31:48 -0700 (PDT) In-Reply-To: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> References: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> From: Michael Shulman Date: Thu, 19 Jul 2018 08:31:48 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] What is knot in HOTT? To: Ali Caglayan 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=BoEvrHi4; spf=neutral (google.com: 2607:f8b0:4002:c05::233 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: , This does seem like the kind of problem that Cohesive HoTT is designed to solve. You could define a knot in a purely topological way as a map from the topological circle to the topological 3-sphere, fatten it up into a tubular neighborhood to express the topological 3-sphere as a pushout of the tubular neighborhood of the topological circle and a complement, then apply the shape functor which preserves pushouts to obtain the homotopy-theoretic data described by Egbert with the homotopical 3-sphere as a pushout of the homotopical circle and some other space. On Thu, Jul 19, 2018 at 1:55 AM, Ali Caglayan wrote: > From what I have seen knot-theory has been very resistant to homotopy > theoretic ideas (not classical ones). One 'clean' way of working with knot > theory is to do so in the context of differential geometry. Cohesive HoTT > supposedly can develop adequate differential geometry but at the moment it > is very undeveloped. > > One of the difficulties with knot theory is that (classical) homotopy theory > in HoTT isn't really done with real numbers and interval objects, which is > needed if you want to define notions of ambient isotopy and such. > > I think the main difficulty here might be that HoTT is great at doing > (synthetic) homotopy but not topology. The two can be easily confused. How > do you take the complement of a space for example? > > I could be wrong however but this is the conclusion I got when I tried > thinking about HoTT knots. > > -- > 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.