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.9 required=5.0 tests=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,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-lf1-x13a.google.com (mail-lf1-x13a.google.com [IPv6:2a00:1450:4864:20::13a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1ede6cff for ; Wed, 20 Nov 2019 21:02:19 +0000 (UTC) Received: by mail-lf1-x13a.google.com with SMTP id x23sf203967lfc.5 for ; Wed, 20 Nov 2019 13:02:19 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1574283738; cv=pass; d=google.com; s=arc-20160816; b=OD8E5Gf+AGmb8nWqSKzj948Dq8Jbaj5t+eAIvLXj3qhEzVI+CGr0NbszIzcxv7PMEn 10SLIhJ3CHT/k6MtKOuHd5vHPiCcyff6Cy4weYE0btsiBTf2yEkETbkRBNJ1mfUiC1iK 9n/ivzyj0gAS+qr1bMalMcrk3PVY6Fzu5yLegPX28AExOcx3VxgzckMfRhNwvWUjDnAr eyILfJW/GvaeIVEuM40S+f9qaErbDHVr4yYyCytyZxh3B4djsKsWKAbRQAsNP0hX6gyq 5iygqtfGLvxOUolwPKYNbT3SvI0nRpxQHFrfGVNjlvRdRgrEx6lZfnR9uqXJ55roUrSN Kozg== 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 :in-reply-to:references:mime-version:sender:dkim-signature; bh=Wuv2N6HRQVlRakgeLY2DAZ9/y8eFd1EmMOjUO4vpKew=; b=I5xkQqE81hiGIFz0iYTS8IfQ8jJPQMTJGbyThJehc3xPzg1kY+A6l6oFQomgN0iZVW fW/W0iFi0GpJkdA5IOY4dPulq3CSBxyOP7t6CHGDMdXgXEt2xfpvul7sP7eHNsIb694Y /XHTNEuD8y7/tWYIRUcpucID9WgylmhyTahYMjXZHoz3TBJ6u3s2vjWhG63EnkvyYfFd x1dCiBIXG6eH1nhYLVShh+Oxcwv/iestbu8bPzNmRRwWtH1pGS02GeHnjj5oWk6V+cM0 CNdapyvg1HizoggSprhXGsGRgdgvtNcDlm6TC05CzbHq41eQ2ipt7EVWas0swT9ErACN ufDA== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of mphmphmph@gmail.com designates 209.85.208.173 as permitted sender) smtp.mailfrom=mphmphmph@gmail.com 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:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=Wuv2N6HRQVlRakgeLY2DAZ9/y8eFd1EmMOjUO4vpKew=; b=sxq5kHXC5Mef9MWs+i2CMGELoLXYPuaSVQBLLC9DtykhL4tsJx9gVQsEEGguN9rOGm 1DPoRJKSQn5Y4aaHjw0BV9hDeHvxCsyff4qZwXbOhRd3lgVQkx/bUEPF9aUp1hXoE3+n jOHmypTrp7FzTTyRDztcbV0A3Y9/AGpegPaVRpWxIGTdvdXPaVj8+lllMRElXnEV7ZmJ wR7Gc9yMnmAYKcJoZ6D7Qm23DvA5moo3KvcmcOXmhO8MCt32x5nuFHMYHTAHtYtDQpLT +F/qjl4X5Rimvn8CBUPBrWcD5H0eUcNvH+KBg3eJ4d7oYHqIQJ13OfK24jfEzwXH5Fm+ m4aA== 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: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=Wuv2N6HRQVlRakgeLY2DAZ9/y8eFd1EmMOjUO4vpKew=; b=YbDqTvpNOAFOZj5LHI2v3827CypXlJiERBRmlUo5ykKF0R7Jx7WA1flx3CmGwzusR8 Yu/YnDzOAYLx8iqPfVy0KYIYb/OWGwDPfzW1IrCwNQgjsA8znQ+6+BYQ6HnardHjy1Q+ wTDjAavzJGXZJBw/gifjmPLbWGcvxZd+5PXqS1AH3KSkftkODGuMey7MIU69iij20pRF 2LqWK36GU2QDhlEejgNnw7XooWjKNdzILaMra2etNsAEuH/IsvjODaAlTuv5RmkrU80o vLQAA0WldoX3OHmxquCffWHolEcXXcRcCNMEvvrq3ynfC1/ij8nzop3jhXh/MgsDjjor P35A== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: APjAAAXt1Wi1q2i4apIGVKNVKHLtJEQJdv6JNpxxhsPDL5LiXwopRsaf w0NqrqH5QBKaF3qIwfY2pow= X-Google-Smtp-Source: APXvYqwyaK9kKl7HxdM5qma2yaXpiOkPyWNA3n4JRL7RHE97AThJNQpxH2FnroESX8rb6pCCsmTFKw== X-Received: by 2002:a19:cc08:: with SMTP id c8mr4524219lfg.124.1574283738748; Wed, 20 Nov 2019 13:02:18 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a2e:8ed1:: with SMTP id e17ls666391ljl.2.gmail; Wed, 20 Nov 2019 13:02:17 -0800 (PST) X-Received: by 2002:a2e:98d4:: with SMTP id s20mr4580990ljj.128.1574283737875; Wed, 20 Nov 2019 13:02:17 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1574283737; cv=none; d=google.com; s=arc-20160816; b=TSzx5/TZFBwtKU6fV7T/nwqZQkXSwW/qs+WuOE3ZHBwhn5QDXJNFTgYEY4ZEZAWHid 9k81zd/jEJR0JFH6OEoZhAw5DZExEr8xVv/weYjSWa0w2WV/wPbKQP4brpUbsctjCxuh F2gHfakm8pHeJlZpC04OgqN+Q+lft2s4A6AX09XqCckq4jzcG4pFg4l0vSOo7vV7dBVz fLZ/gy1KKICSfswQ9yhvrsjnPxgYq9Bdkm9CalLVxa9FcWtkBQMOJpSXEISKO7cKghgH x/kz94e3JEASgwSTxxOdhBSvDuETHpHx/dttwD22atHY5xJmbs4XXq1wiwLkZZeXJ+f2 hTgg== 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:in-reply-to:references :mime-version; bh=CW5X+IPQ1rE470GQfk64Ev6DSfx1wfsp04AqogJ7HuQ=; b=HFirBcwiAyRvAmqSbIYk4V2NFtPP+IPc4d2S5EWFX8SNPuSNY23SA3k80je/XF/aTi 4he1u5lS+DnJbtvKrY+fQixX/OOKizcGpUS7zPlhQLTV+VKZN0zwSObTvd9SJWM/tUdx y51x0x2SYiuUdFFFBhd3UC+booFe+yfHyg71pmrsi2IGasssESHRTIlmX8445nsiCjoJ qLGqzopuf0HP7RnaFA5db7QIC2wChnfRK4pWJFxU84TNjdZxbuGo9BPT5YP8ngDFO22Y ZjpKoa7YXS9I0oOXbC/tcXZDt/ZvK0pyczI6eDkFDuV7rtr8SuSPwToJdW7bnK5ecGhO RbrA== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of mphmphmph@gmail.com designates 209.85.208.173 as permitted sender) smtp.mailfrom=mphmphmph@gmail.com Received: from mail-lj1-f173.google.com (mail-lj1-f173.google.com. [209.85.208.173]) by gmr-mx.google.com with ESMTPS id j14si28188lfm.2.2019.11.20.13.02.16 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 20 Nov 2019 13:02:16 -0800 (PST) Received-SPF: pass (google.com: domain of mphmphmph@gmail.com designates 209.85.208.173 as permitted sender) client-ip=209.85.208.173; Received: by mail-lj1-f173.google.com with SMTP id g3so658556ljl.11 for ; Wed, 20 Nov 2019 13:02:16 -0800 (PST) X-Received: by 2002:a2e:970a:: with SMTP id r10mr4593034lji.142.1574283736329; Wed, 20 Nov 2019 13:02:16 -0800 (PST) MIME-Version: 1.0 References: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> In-Reply-To: From: =?UTF-8?Q?andr=C3=A9_hirschowitz?= Date: Wed, 20 Nov 2019 22:02:05 +0100 Message-ID: Subject: Re: [HoTT] What is knot in HOTT? To: Ali Caglayan Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000e1352c0597cd7eec" X-Original-Sender: ah@unice.fr X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of mphmphmph@gmail.com designates 209.85.208.173 as permitted sender) smtp.mailfrom=mphmphmph@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: , --000000000000e1352c0597cd7eec Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi! My guess would be that differentiability is irrelevant for knot theory. You could rather consider closed subsets homeomorphic to S^1. For instance you could restrict your attention to "paths" consisting of injective sequences of integral points P1, ... , Pi, ..., Pn=3DP0, where PiPi+1 is parallel to an axis and of length 1. There is probably a corresponding notion of "discrete" isotopy among such paths, so that if two such paths are continuously isotopic, they are also discretely isotopic . As a consequence knots now live in Z^3. So you can take the higher inductive type H with Z^3 as set of points, and the above (length one) intervals as generating equalities, and study "synthetic knots" in there. The first thing to check is probably that any path in H is homotopic to a path obtained from a sequence of generators. I am not sure at all that such a synthetic knot theory could be fruitful May-be more interesting is to fill the holes in the H above by adding generating 2-cells one for each elementary square and 3-cells one for each elementary cube. It is not so clear how to do it if you want these cells to be "invertible" More generally given a triangulated variety of dimension 3, you may try to specify as above a higher-inductive type, so that you could try to formulate (and prove...) a synthetic Poincar=C3=A9 conjecture. Sorry for divagating slightly too much! ah Le mer. 20 nov. 2019 =C3=A0 20:13, Ali Caglayan a =C3= =A9crit : > 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 manifo= ld > (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 kn= ot >> theory is to do so in the context of differential geometry. Cohesive HoT= T >> 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 suc= h. >> >> 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. H= ow >> 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-8= 751-9b0a342e9bdf%40googlegroups.com > > . > --=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/CAHPPr6zWU1VN7J_NXTJQ6ZuLc3TjrJ7yfJwMDqPuVu005%2BJqzA%40= mail.gmail.com. --000000000000e1352c0597cd7eec Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi!

My guess would be that differentiability is irrelevant for knot theory= .
You could rather consider closed subsets homeomorphic to S= ^1. For instance you could restrict your attention to "paths" con= sisting of injective sequences of=C2=A0 integral points
P1, = ... , Pi, ...,=C2=A0 Pn=3DP0, where PiPi+1 is parallel to an axis and of le= ngth 1. There is probably a corresponding notion of "discrete" is= otopy=C2=A0 among such paths, so that if two such paths are continuously is= otopic, they are also discretely isotopic . As a consequence knots now live= in Z^3.
So you can take the higher inductive type H with=C2=A0 Z= ^3 as=C2=A0 set of points, and the above=C2=A0 (length one) intervals as ge= nerating=C2=A0 equalities,=C2=A0 and study "synthetic knots" in t= here. The first thing to check is probably that any path in H is homotopic = to a path obtained from a sequence of generators.
I am not sure a= t all that such a synthetic knot theory could be fruitful=C2=A0 May-be more= interesting is to fill the holes in the H above by adding generating 2-cel= ls=C2=A0 one for each elementary square and 3-cells=C2=A0 one for each elem= entary cube. It is not so clear how to do it if you want these cells to be = "invertible" =C2=A0 More generally given a triangulated variety o= f dimension 3, you may try to specify as above a higher-inductive type, so = that you could try to formulate (and prove...) a synthetic Poincar=C3=A9 co= njecture.

Sorry for divagating slightly too m= uch!

ah



Le=C2=A0mer. 20 nov. 2019 =C3=A0=C2=A020:13, Ali Caglayan <alizter@gmail.com> a= =C3=A9crit=C2=A0:
It seems to me that "differentially cohesive = HoTT", whatever it ends up being, is exactly the kind of viewpoint nee= ded to study knot theory. The following characterisation of knot theory (I = think?) due to Allen Hatcher might make this more apparent:

<= /div>
Knot theory is the study of path-components of the space of smoot= h submanifolds of S^3 diffeomorphic to S^1.

So you= need to be able to talk about a space being smooth, pick a smooth structur= e for S^3 and S^1, what it means to be an immersion into a manifold (subman= ifold) 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 w= e have some workable theory of differential cohesion. Currently we only hav= e real-cohesive versions of HoTT.

Some starter que= stions would be:
=C2=A0- Can you characterize the trivial knot.
=C2=A0- How do you define the "connected sum" of kno= ts.
=C2=A0- How do you show every knot has an "inverse"= with respect to the sum.


On Thursday, 1= 9 July 2018 09:55:55 UTC+1, Ali Caglayan wrote:
From what I have seen knot-the= ory 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 c= ontext of differential geometry. Cohesive HoTT supposedly can develop adequ= ate differential geometry but at the moment it is very undeveloped.

One of the difficulties with knot theory is that (classic= al) homotopy theory in HoTT isn't really done with real numbers and int= erval objects, which is needed if you want to define notions of ambient iso= topy and such.

I think the main difficulty here mi= ght be that HoTT is great at doing (synthetic) homotopy but not topology. T= he two can be easily confused. How do you take the complement of a space fo= r example?

I could be wrong however but this is th= e conclusion I got when I tried thinking about HoTT knots.
<= /blockquote>

--
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 ht= tps://groups.google.com/d/msgid/HomotopyTypeTheory/b886590f-c92b-493b-8751-= 9b0a342e9bdf%40googlegroups.com.

--
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://g= roups.google.com/d/msgid/HomotopyTypeTheory/CAHPPr6zWU1VN7J_NXTJQ6ZuLc3TjrJ= 7yfJwMDqPuVu005%2BJqzA%40mail.gmail.com.
--000000000000e1352c0597cd7eec--