From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCR3VC42QYFBB26KYDNAKGQEGKXHRLQ@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 autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-wr1-x43b.google.com (mail-wr1-x43b.google.com [IPv6:2a00:1450:4864:20::43b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 00102a07 for ; Thu, 19 Jul 2018 05:45:16 +0000 (UTC) Received: by mail-wr1-x43b.google.com with SMTP id z16-v6sf2966304wrs.22 for ; Wed, 18 Jul 2018 22:45:16 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531979115; cv=pass; d=google.com; s=arc-20160816; b=Nuxf7RKScG+eM9BURYSZdWMtkMgxac4ofgJE1TiU1QjIBaAdWV7gedVbFUHC4e3Hr6 kgpEsNEgpMQDtqgIo2xvrM9UwsGc+zkifcEzKA5Lx2IhBneuonxyDMgev6ZgA6nJftMt o3akwu1ZOh+cKp96o+8dFicyRnr0R0PcSk80SqZ5smfj9PKJ4xaGsJV4i76/k/L/GVhz YBS0k6Iirat9ClA49DH3MxxdGfIxXRk6oylxANb54zuFKRNlkzp8lesxY8NVEWguYefm V7cj+8wSyB2DllxguZ+ZeAIJfl6HlMaXOk8bbTfP39CMb4sV7pAfgSaDzO7uUH4g1hoc AckA== 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:dkim-signature :arc-authentication-results; bh=tS5CA1MNzC8hpuu6KbgyEp54P57mRH2lptF3QLBk+Wo=; b=SjSshqdMJdgVNSoxvhXhN5V4ASVqaoETHWge8GkzfptA6hqeNeC9qSBWoW+iyhXteD cfDMa8aoOWSIpyuL6Zgn7KkCPvT7EHwKp+VHkhPeVp7vL44ZsKNliZlIp7vkzcgPjQim JrdsLm8cHJQabfSAgAf/q5BLfE7nm/spshBuKwVFlf5xGp0mvMSccV/TfliRJL9T+0hL TfradN+4dwYYjBlDAlqFm56TG4TffWa2zXOrljtUsf6ealjveSpZOOGiSJcl0+k6v3BV pQVcIW4j7cmi1z11bjG04CVSfSIlLmgXtQxz7bRuMoq4M4lSc2dmMUfWKiL0Lt/zJYiq a34A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=n7vYvN8x; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:400c:c09::244 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=tS5CA1MNzC8hpuu6KbgyEp54P57mRH2lptF3QLBk+Wo=; b=ZBVOPZjJJhaZJzFYZAiGgSBCGeWkIeJB2+9bWQxRTnIlTe+nDsJZsJdNvMLyNx6o7y Pgxx9bJA2bcsE/ixUkm4TN20+jxeUjzArxqKUs23iBYJ9fr+gsAQNjvji4e6yPupkQHQ OZoT9YOgWJRrI4KlT6AUt9yMs9CkO0xOI73VdmyGrnghdIbxaB5EJLtP55jl3+U4BcdM 0UY82o7RZ1NTpagl19Wwa1JzuCO1Xheq9RywIehe/S7kndq5x7TaizIC24kJ29XTAR+v ChuGhOwqiENMFkBhHC6sMu7uTuHFOtejqk/uuvsKDiN815XpI5duqpC7Plt5nIpxypHE HkWQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=tS5CA1MNzC8hpuu6KbgyEp54P57mRH2lptF3QLBk+Wo=; b=AI/csC4vvvv/LTEQIpRTyMjoBllv0AM7DkMBgYrJ674xuo/wTD2i/8VVptWvXCL2+c WqgvDgvRfLmmgP3AJpqK16+VzcUSllKIW4J2Xao7Wm5ulwcYxU6iyj9VZFD0tvMHk927 VeaH+Xbmf3mCOywTqd1aW9w0WFYUacC0k0UZc00tTsqwqYpPBv+OanMGEvAdSSuPNhp1 edGf91YjtYsgFqQ7BN0diThW4BlDEeUksupBX4YsAfgzvCgKv1t04boAydhWe2TAbHr9 GMQaIdyvUBPSx4jZCrK7ljHX6/h6rHcKRQnn33NvEP02+7pwY/JUKwiRTv9kfXEW8QZl Zb0A== 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=tS5CA1MNzC8hpuu6KbgyEp54P57mRH2lptF3QLBk+Wo=; b=PbndOPKB3vXM+zGNyLrj2MohIUEMgQKD0jdz5FJjceTbLLoIOw6hBtgdV1lpvVgmrS aTOYOqtStY9VJr/7tbrIEz4IXhMnmZGa7lyr9Vh4uscDGiVwdrbOpx8J/wwG2XDV60I3 LIJssKNd0sGzPcfqRiZuJKIZkW1nxiNmlItc9dsf/huJwQmetqFwBaOFLfIsct1qWIas ujelM32h9TcmnQQsMlTDrzIZ1lSg+5Jw32g/ABq1WkyqwfFY2W94h4pBFSs4W1Amy6B8 frotqQYlp9rXKE1h+Jk3yGyBFOtkSiECu9N4FjCT4rdcj0e4LjusR/bGG1/z/HTNFG9U SGkg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGCtbf7YwG2Uzxvvre+fxw8/RXoLIEidcnDsSTGdQS/aO3TWGY2 n4nPeT0dmOUcTNHjdj0/ytA= X-Google-Smtp-Source: AAOMgpexqBR4UwyajoHVcSe/eXMWA3HN7O7WnvtoMgi44yRkw7XQw37kwp44c8CGfT38uN7GxcVd0Q== X-Received: by 2002:adf:9c91:: with SMTP id d17-v6mr99362wre.6.1531979115143; Wed, 18 Jul 2018 22:45:15 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:8c05:: with SMTP id o5-v6ls818479wmd.3.gmail; Wed, 18 Jul 2018 22:45:14 -0700 (PDT) X-Received: by 2002:a1c:968b:: with SMTP id y133-v6mr426771wmd.22.1531979114628; Wed, 18 Jul 2018 22:45:14 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531979114; cv=none; d=google.com; s=arc-20160816; b=goGbVVd6luvLVqXT5xk+SAGD+nwyOKO9oOEyFvFIagpIM5+Y65tv0mpjOzUJkov9oD FUXuiiARmytYLB1iLAg8/pJK1Tf2yJ2yZhrIiYbf/Fz0Em0p1R1kDXARQSzRPKUWQoy/ SQj1AnF8tJulGkH2Q7EmWfjdS/w1BvKIY0BwfN9Fk9x5CiNuvkQGZRHeYWn63Ms0tKIT IsQVVccuGeVsZ4fkNofMsbYVR36Vua8Dmm89XotSN+qnv9vJFNn2JK2srcPf6sQyzP33 uUN11lXKCwc8jYuTH+n66W3Kc06XeUblDtC9xWOeIoFTmR/v5IzFvMB76CEQzZuffoUE qbFA== 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=cHCed4u3pnhloaEwtXs7Np0NtYPmgx2ooT5XWV4REUk=; b=ceS/Clu4O0sGAkfRrfz1Y28HYikH1IqYdG4jz7vd5nvlJrxG2z1sKN8Meww2bqaEbd rNFzVg7HRGcI99UP1ySlbJXgYiHDk640g3WVHFY9fvONGTake0BCXxRImAZLPhLJV14c YUXz5bnEe0a4id+5E0c6YGLs6FaIx/T9/qPUA9++azMsxtahoKcA/AdAhww2ca7sCXB0 J+A4R7e9wc2f93ukoGmYf25LgTnYxMeheLiiyBPDOvfaY5bf0JaMC/fqbbPfolqJrCP4 Mbjv2IyV62mezZZf75K1C3kYr8PCbS1ivX3MkUyjTmzQ2DEastjTM5hcx33vM6KnN6WG 1Hyg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=n7vYvN8x; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:400c:c09::244 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm0-x244.google.com (mail-wm0-x244.google.com. [2a00:1450:400c:c09::244]) by gmr-mx.google.com with ESMTPS id o21-v6si32463wmc.1.2018.07.18.22.45.14 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 18 Jul 2018 22:45:14 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:400c:c09::244 as permitted sender) client-ip=2a00:1450:400c:c09::244; Received: by mail-wm0-x244.google.com with SMTP id h3-v6so4422166wmb.1 for ; Wed, 18 Jul 2018 22:45:14 -0700 (PDT) X-Received: by 2002:a1c:3282:: with SMTP id y124-v6mr3288875wmy.11.1531979114295; Wed, 18 Jul 2018 22:45:14 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:adf:9a8f:0:0:0:0:0 with HTTP; Wed, 18 Jul 2018 22:45:13 -0700 (PDT) In-Reply-To: References: From: Egbert Rijke Date: Thu, 19 Jul 2018 01:45:13 -0400 Message-ID: Subject: Re: [HoTT] What is knot in HOTT? To: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="000000000000e9357c057153aed1" X-Original-Sender: E.M.Rijke@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=n7vYvN8x; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:400c:c09::244 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=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: , --000000000000e9357c057153aed1 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Dear Jose, One idea I have been playing around with is to define a knot to consist of a map S1 -> S3 together with a type X equipped with maps S1 x S1 -> X and X -> S3, and a homotopy witnessing that the square S1 x S1 ----------> X | | | | V V S1 -------------> S3 commutes, and is a pushout square. The idea is that a knot is a topological embedding of S1 into S3. We can fatten its image up to an embedding from S1 x D2 -> S3, where D2 is the unit disc. Its boundary is the torus S1 x S1, and the embedding S1 x D2 -> S3 also has a complement. Then S3 should be the homotopy pushout of S1 and the complement of the subspace S1 x D2 in S3= . The problem is of course representing known knots in this way, which I don't really know how to do. For example, what is the homotopy type of the complement of the trefoil. This is probably known in the existing literature about knots, but I must admit that I don't know it. And also, what is the embedding S1 -> S3 for the trefoil knot? The fiber inclusion of the Hopf fibration perhaps? That would be a guess. I would be very interested to hear if others have ideas on this topic. And just to repeat myself, I also don't know for sure if the above is a correct representation of a knot in HoTT. With kind regards, Egbert On Thu, Jul 19, 2018, 1:18 AM Jos=C3=A9 Manuel Rodriguez Caballero < josephcmac@gmail.com> wrote: > Dear HoTT group, > I'm thinking in the following question: What is the type-theoretic > definition of a knot in HoTT? > > Thank you in advance if you have some answers. > > Sincerely yours, > Jose Manuel Rodriguez Caballero > > -- > 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. > --=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. For more options, visit https://groups.google.com/d/optout. --000000000000e9357c057153aed1 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear Jose,

One idea I have been playing around with is to define a knot to cons= ist of a map S1 -> S3 together with a type X equipped with maps S1 x S1 = -> X and X -> S3, and a homotopy witnessing that the square

S1 x S1 ---= -------> X
=C2=A0=C2=A0 |=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 |
=C2=A0=C2=A0 |=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 |
=C2=A0=C2=A0 V=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0 V
=C2=A0 S1 -------------> S3

commutes, and is a pushout square. The idea= is that a knot is a topological embedding of S1 into S3. We can fatten its= image up to an embedding from S1 x D2 -> S3, where D2 is the unit disc.= Its boundary is the torus S1 x S1, and the embedding S1 x D2 -> = S3 also has a complement. Then S3 should be the homotopy pushout of S1 and = the complement of the subspace S1 x D2 in S3.

The = problem is of course representing known knots in this way, which I don'= t really know how to do. For example, what is the homotopy type of the comp= lement of the trefoil. This is probably known in the existing literature ab= out knots, but I must admit that I don't know it. And also, what is the= embedding S1 -> S3 for the trefoil knot? The fiber inclusion of the Hop= f fibration perhaps? That would be a guess.

I woul= d be very interested to hear if others have ideas on this topic. And just t= o repeat myself, I also don't know for sure if the above is a correct r= epresentation of a knot in HoTT.

With kind reg= ards,
Egbert

On Thu, Jul 19, 2018, 1:18 AM Jos=C3=A9 Manuel Rodrigu= ez Caballero <= josephcmac@gmail.com> wrote:
Dear HoTT group,
=C2=A0 I'm thinking in the follo= wing question: What is the type-theoretic definition of a knot in HoTT?

Thank you in advance if you have some answers.
<= div>
Sincerely yours,
Jose Manuel Rodriguez Caballe= ro

--
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@go= oglegroups.com.
For more options, visit https://groups.google.com/d/optout.

--
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.
--000000000000e9357c057153aed1--