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=-0.7 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,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.2 Received: from mail-ot1-x338.google.com (mail-ot1-x338.google.com [IPv6:2607:f8b0:4864:20::338]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2628d049 for ; Wed, 20 Nov 2019 19:13:19 +0000 (UTC) Received: by mail-ot1-x338.google.com with SMTP id e6sf257173oth.17 for ; Wed, 20 Nov 2019 11:13:19 -0800 (PST) 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=pk0IMul8byU0xfNi/Zoipi/6ic4jQ+XvXdOatXXuzr4=; b=RYANC1gTt2nJZliGL9eixuKeb7Ovi+k5RZCBFJvkNJExDHjnkFmZNNrndGnrBx9PqI myBC+TKnvYqG1YWraGGYci3D/IvI+JaNkp3Cg5EZRMgox8gN6mg4eknagblyzBaDRmf5 8x3DkzMJXfqCwWZDCoepl782aS13HgZCI3wvEwlHAc5lOmuIk0GeF5OdqTxh71N+QKBR q+p80QdFivkhe/LQ+zVoYm42rxjBS9qRt05GuQTlm2ZGAwZwjeS12D5Vh/iIFkHSDe9q 3KX9KE83QzL/FMY/NDnOn2d5nmH+Gh9R+kaY/VxSyBdueSMKijcB0IERSS+oC/pKcaOE sB4g== 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=pk0IMul8byU0xfNi/Zoipi/6ic4jQ+XvXdOatXXuzr4=; b=vIWfXHm7db039cxLI7+LHdGnyOc42M5jR1BSRS26LZBL8IEt5SS58RplXRCAhdM9ID Lf19XhooAGZa1wv9QstWJ8m3V/7ifBYYyOvkHmGa4D0h40Fqhb0N3wf8qxw1/CISFQOY Etgfk6lz0oKCM7diMN68VmYSljTSy5WVF+uqaj28RKiRcWOrFzwzlzxNMh4EaeDdu2ct Qf8oJ/WT+RiUHa067gzZcwoCy/he9z0b90DJVc3VXQKix9QvOO2bZJv/eSU7gdjptj4P 4K2BJue2Tzs8L+dhShQhmJCj4T+a5iVxA3SzuCTqeUJsCmXUoj8q5sd4UExRWDbqUu8e eRjg== 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=pk0IMul8byU0xfNi/Zoipi/6ic4jQ+XvXdOatXXuzr4=; b=tBBQNL+nvYI79YXDhcSNK1+VauXLz+E0mD6yNN6Ou9l3MTQdtCHejAovg41rOxdxgd 2Q92CSw8lUWYneRoXnpwEd8g/ZBqTn9pIN5fUnfLJ5jFWf23ZO8UPCtedINruLQjbFo7 jbv2xCteQ6yvy7AWQkeCreQNZCCGZa/jTXHNeL0ajmRatkP0dol3Xjo401fdbXRGHNwu hDIM38OMAwSKyiZF0lXSJqYXcCstj8lA+gvrHsqYpvjFLfgLwQeDeb9N4FaLdLsoRKpZ F50uYOOencs5hiUVVoH6hbaljoO9bapo7KWZnOKLXtGzLaCJPO4Y6yIBqRWWUFtOZMhw UtbA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAVrxQHFLt16IJuj+IKJ2sVNNYUlUQobHVrBpvpCdLgxMXFDQ731 +Aga2NfhrRO8BlIjbfp2yIc= X-Google-Smtp-Source: APXvYqwF7vEmPnVYy3DCduLyKUnZRHZ8ZNr7bt1oCBbkx2sfjmYjstkN4Pko1WF/u4394fXyJMDHvw== X-Received: by 2002:a9d:5543:: with SMTP id h3mr3293361oti.33.1574277197979; Wed, 20 Nov 2019 11:13:17 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:aca:3408:: with SMTP id b8ls511952oia.16.gmail; Wed, 20 Nov 2019 11:13:17 -0800 (PST) X-Received: by 2002:aca:6006:: with SMTP id u6mr4259063oib.137.1574277197425; Wed, 20 Nov 2019 11:13:17 -0800 (PST) Date: Wed, 20 Nov 2019 11:13:16 -0800 (PST) From: Ali Caglayan To: Homotopy Type Theory Message-Id: In-Reply-To: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> References: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> Subject: Re: [HoTT] What is knot in HOTT? MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_2250_1507047532.1574277196571" 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_2250_1507047532.1574277196571 Content-Type: multipart/alternative; boundary="----=_Part_2251_2131798871.1574277196571" ------=_Part_2251_2131798871.1574277196571 Content-Type: text/plain; charset="UTF-8" It seems to me that "differentially cohesive HoTT", whatever it ends up being, is exactly the kind of viewpoint needed to study knot theory. The following characterisation of knot theory (I think?) due to Allen Hatcher might make this more apparent: Knot theory is the study of path-components of the space of smooth submanifolds of S^3 diffeomorphic to S^1. So you need to be able to talk about a space being smooth, pick a smooth structure for S^3 and S^1, what it means to be an immersion into a manifold (submanifold) and diffeomorphisms. This is just stating what knot theory ought to be, I have no idea if this viewpoint can actually tell you anything until we have some workable theory of differential cohesion. Currently we only have real-cohesive versions of HoTT. Some starter questions would be: - Can you characterize the trivial knot. - How do you define the "connected sum" of knots. - How do you show every knot has an "inverse" with respect to the sum. On Thursday, 19 July 2018 09:55:55 UTC+1, 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. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googlegroups.com. ------=_Part_2251_2131798871.1574277196571 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
It seems to me that "differentially cohesive HoT= T", whatever it ends up being, is exactly the kind of viewpoint needed= to study knot theory. The following characterisation of knot theory (I thi= nk?) due to Allen Hatcher might make this more apparent:

Knot theory is the study of path-components of the space of smooth s= ubmanifolds of S^3 diffeomorphic to S^1.

So you ne= ed to be able to talk about a space being smooth, pick a smooth structure f= or S^3 and S^1, what it means to be an immersion into a manifold (submanifo= ld) and diffeomorphisms. This is just stating what knot theory ought to be,= I have no idea if this viewpoint can actually tell you anything until we h= ave some workable theory of differential cohesion. Currently we only have r= eal-cohesive versions of HoTT.

Some starter questi= ons would be:
=C2=A0- Can you characterize the trivial knot.
<= /div>
=C2=A0- How do you define the "connected sum" of knots.=
=C2=A0- How do you show every knot has an "inverse" wi= th respect to the sum.


On Thursday, 19 J= uly 2018 09:55:55 UTC+1, Ali Caglayan wrote:
From what I have seen knot-theory has = been very resistant to homotopy theoretic ideas (not classical ones). One &= #39;clean' way of working with knot theory is to do so in the context o= f differential geometry. Cohesive HoTT supposedly can develop adequate diff= erential geometry but at the moment it is very undeveloped.

<= /div>
One of the difficulties with knot theory is that (classical) homo= topy theory in HoTT isn't really done with real numbers and interval ob= jects, which is needed if you want to define notions of ambient isotopy and= such.

I think the main difficulty here might be t= hat HoTT is great at doing (synthetic) homotopy but not topology. The two c= an be easily confused. How do you take the complement of a space for exampl= e?

I could be wrong however but this is the conclu= sion 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.
To view this discussion on the web visit https://groups.google.co= m/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-9b0a342e9bdf%40googleg= roups.com.
------=_Part_2251_2131798871.1574277196571-- ------=_Part_2250_1507047532.1574277196571--