From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCQ657FO5MEBBHFEYHNAKGQES7PZLVI@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.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-oi0-x23f.google.com (mail-oi0-x23f.google.com [IPv6:2607:f8b0:4003:c06::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id a1b9ce94 for ; Thu, 19 Jul 2018 08:55:57 +0000 (UTC) Received: by mail-oi0-x23f.google.com with SMTP id l26-v6sf6677044oii.14 for ; Thu, 19 Jul 2018 01:55:57 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=W2gpJJI8lXCLXNg75ZmOdznnZ7lSmaFCbIUvrXsLcaU=; b=TJ3aH7JtsovhcjvG+4vdTvoXUd/RaOXcOp8DNNGaCjoNfJ7kYpo5piRo1TGWAN+TKL JMdkUbCH/PTaKIu1uTCMMVLnRLOZ4JG6lwf5QIWaHVIhaSbXgF9zX2VMM2+hNtSzIFtY YJgu9Q5M5vGm0f8VZdmlqD86lZQbFkj6C6BCQFa5iaqHTJfTJI2nFs6I7vij3zh7ffnK hYTRTP5H5AduGgyjbTo+tOmGAjfNNehoR1f1lYrLxp7csurDEkwzyEImCyQn85IqWJnm R8JmhUjYmYDrHh/GCTFfevCQKuc23ya1ikGW7AXhrMaHeQau3iZdDBombpLZEPEpAKqw 8fPg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=W2gpJJI8lXCLXNg75ZmOdznnZ7lSmaFCbIUvrXsLcaU=; b=VvT1R3PNryS13ROkuzkogqKZCYSctx/Wi+dnnYkkgiOS7+8JV9IlINHMfEtSGb4FQi GxwKpA2tFfM8ENkUXMBoQHUMc9ikMh8/JJhUJVj+bRVmD3LrRTUBtPJV1S+iXzC1vlVt dGRD8bPikmVZjI0Qneoid+xO6QqzEaE9k3QquX6zvXnp7QjCz19uKLSpWZy1AjK6TUxy F3/0OYLWNjXQu690CnL6VQ4/H1mOczUAYrRco9COA1Cva7OK0RAPYgBf7yG0iZ/587pZ uMLbwIov++y2YMxeEpdv3VJFMoSPw2+znCIVre66TB+nEgFeMHBCi9ggm16lMZf6oZLD SFEg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=W2gpJJI8lXCLXNg75ZmOdznnZ7lSmaFCbIUvrXsLcaU=; b=b2gX2/wPlfO+wYUmcqKjkMjzehuKoKgiYOqBCo10Ix4KAah7bl3qb6zty+hv8FlZwy F0vYAk+PrKrzHEy62maeTOfzfuL3Fs0/tVkFTwEnwtk5QmSpLkycXq6GWLa6aAHB58xt DHw9sJxG3V/Wvw8sG7u2hjdTCgjsh86zi1ieU1mUatb9hPQE3dp1VXSD61Nd1ouBUYsG 8moE024CqtLd8K6NP4VT+JvhypdmqdpPPyBZ7QjzsoBCcn9sa3wRo90xsk45rweYCx0c sywlM++i7fEnawvtfkIykeAMxPi9jiU6G3XO2UgqAHBL5XaMU0RfZ1QCOn6kjIVBGy0B iDSQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFcuj1a3SXmAMZCz8AA3L1+G4i+hBMFDKX5qHgMCokgP+0sWhiy 2F4VREjF6JxLVBnK+3bP8WQ= X-Google-Smtp-Source: AAOMgpdHlHFmaPfOaTdCleVjuQomiwi1+4RGxErA6SVznlci7IjXMJxlqCpRUSkPlpgW/zIQbN/eJw== X-Received: by 2002:aca:eb15:: with SMTP id j21-v6mr1798007oih.6.1531990556242; Thu, 19 Jul 2018 01:55:56 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:40c4:: with SMTP id n187-v6ls4481334oia.18.gmail; Thu, 19 Jul 2018 01:55:55 -0700 (PDT) X-Received: by 2002:aca:f495:: with SMTP id s143-v6mr1786412oih.7.1531990555707; Thu, 19 Jul 2018 01:55:55 -0700 (PDT) Date: Thu, 19 Jul 2018 01:55:55 -0700 (PDT) From: Ali Caglayan To: Homotopy Type Theory Message-Id: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] What is knot in HOTT? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2111_1993649100.1531990555214" X-Original-Sender: alizter@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: , ------=_Part_2111_1993649100.1531990555214 Content-Type: multipart/alternative; boundary="----=_Part_2112_74510527.1531990555215" ------=_Part_2112_74510527.1531990555215 Content-Type: text/plain; charset="UTF-8" >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. ------=_Part_2112_74510527.1531990555215 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
From what I have seen knot-theory has been very resis= tant 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 geomet= ry but at the moment it is very undeveloped.

One o= f 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 gre= at at doing (synthetic) homotopy but not topology. The two can be easily co= nfused. 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 &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
------=_Part_2112_74510527.1531990555215-- ------=_Part_2111_1993649100.1531990555214--