From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDPYD3663QBBBAX2Y7NAKGQEKTBOZWY@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-io0-x23f.google.com (mail-io0-x23f.google.com [IPv6:2607:f8b0:4001:c06::23f]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id d5429904 for ; Fri, 20 Jul 2018 15:17:23 +0000 (UTC) Received: by mail-io0-x23f.google.com with SMTP id y26-v6sf8618656iob.19 for ; Fri, 20 Jul 2018 08:17:23 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532099842; cv=pass; d=google.com; s=arc-20160816; b=yBrOQHa4N0flP9B+UCK71J6To8duGOT3fUFE2DAjAdt+++OMnhVsgEnIljYXWwPCuC 0l1PMChizITgE9Xzs5bjJUhVhUjkQH7mLghnhLxJSuq5sEGYvrlyBUst0Kwf9EfDKTRr K/uWfKzeTnyZ2hpeuhpa4ilJm1TcjXqV769sTaoV+I8bQHsuw8/D8ESjUNmhzEbkMtev Q09nQyCxUg0WgnvYqemHSyDMZ9yKrYMN8gznMQRHsm6c/Em/vYHkE9IJ141lPHoZ2DPa 8wXM1Odq5fE2rR3jJCp2vBxJ3qlSEiqqVmw01XfanLPQ94kDlGy+FOlHdcOZ0+HTg64K ooEQ== 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:mime-version:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:ironport-phdr :arc-authentication-results:arc-message-signature:sender :dkim-signature:arc-authentication-results; bh=7MnAKb35+EVCgC+fDes5B4Yx6ikAJdRCLC9epm9kIRY=; b=jDGEGitF9IJqh8DMeki0A95jmnNmdCP+xcPnowzFlLM8uEF4RrbbPDlcxO3lj6XLta dxljv1oiKRtBwltCSPJ9ikZ/km9cJNzJvTcp6TfgElUQXGwnZvwLZXA+Yoi5gBbao7m9 az2HVqQ+EL5YvAA4fh6PtWPubNsVuoc1+3S548nzLu9tSDnlMd4CJe4iVwKTDpazwFSJ JNeckTuLyeeZHKiisA6VNJv4GXpe1bciS70dS4e3dORvEuHEoLStgAQRPYGGT8ZAbUSE DymF4ctpoxyErDZvdWyM0Gof0kpJt9piBoA2KirFPXXy37NusejjrPlgzWJ2nFysMwr7 ljFw== ARC-Authentication-Results: i=2; gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=uqam.ca DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:ironport-phdr:from:to:cc:subject:thread-topic:thread-index :date:message-id:references:in-reply-to:accept-language :content-language:mime-version:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=7MnAKb35+EVCgC+fDes5B4Yx6ikAJdRCLC9epm9kIRY=; b=VJgkzDXjdekAkKN15JAvyjtxbYnvfd36WEDivgY2wOlEJgOT5olGQRThwsgfya4yCZ P2qjMBTDHzICdouAXu4n5KXhO3826YJldYA9JiScBR+nKNQUxtM2sYR2BoUpyGRYNdoo NwLUkB4xslHsXFNATWCl78eSGEZfP0yOjj5OzKhh6uhp17Qbb9qAC/dFMddJGj6ThKag bqpN1cgcgbQxM2ZjoZr8jR++3qKd6jSww714vuVLYJrOSrMU0LEZJPlBJf1Fsg807KfM R7zqyYT3l4ilTk9NxDN7t111N5AREDAIgm0Erl7rADvcA2X0pN4GjzlRS5lqDULT2E8t i6sA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:ironport-phdr:from:to:cc:subject :thread-topic:thread-index:date:message-id:references:in-reply-to :accept-language:content-language:mime-version: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=7MnAKb35+EVCgC+fDes5B4Yx6ikAJdRCLC9epm9kIRY=; b=ePu7+K669mMqeiZ1XjN8clU6mxFgLEZD/GxELhFi7rhaOINxnaR09QP3sD7HnI+LQQ k4dp38JvBxqQqu2/K7HNyqMEZzkBVCt9CTX6QEvW+i31XVIkfM4a1d8lOQUXZUUZ2Zix FlXlo4+MhvKOxuj5nYMln3gsQ7oDX66VFbd+NLc1UbtbgqlVGII2tURQ5B3162bMYzrR A1Z1BAQsebiMtEPimgGv8X0BvV6b4CyRDGibnffM1PqgC53DwhLXfJPlmcG9EhxguhCX TxR7Pt1CygZzpmS4E6x+3pz05aiPC86BsxWgqYtTjIhv6PeCeHgU97OBNg+nX2UXOo84 iJRQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGBk9sluJzWmC3vSsUr4fo3KXevsv9dwkWbR85s/jg0QwB+XZv7 WLd3ZsAqJHO+9JZ1tqXattk= X-Google-Smtp-Source: AAOMgpefZayb83lCtkF/ACGfREa//br4oWk1dfppRQnCFxV1V/pURgAzV46WLmtktVeMjmZj9HNXCg== X-Received: by 2002:a02:394c:: with SMTP id w12-v6mr19999jae.3.1532099842413; Fri, 20 Jul 2018 08:17:22 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a02:51c1:: with SMTP id s184-v6ls436486jaa.2.gmail; Fri, 20 Jul 2018 08:17:22 -0700 (PDT) X-Received: by 2002:a02:8782:: with SMTP id t2-v6mr1076666jai.3.1532099842119; Fri, 20 Jul 2018 08:17:22 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532099842; cv=none; d=google.com; s=arc-20160816; b=Z45QJAfJHPugTd4TAvY8w62yWV79M4BYo3N7/X6SH53slAiCSf98Oq14FyaWSzNebP hgUx8qv3IBmjfrdGFxiShD19R2fZ0A62I3VILP9khirlcIbHUpbdqpNEvNSzdFueO1Nj GtwntLGr7qSv+bwoLmVioWOGEmfXJ8xjhpF1GiYcfdHPamagqIps3nD1Yc+Hcarw+/p0 CmqDNWvG0ISWqKZ/PbLNI6q0WrUJl3XkZ+bOyaFNnaayHZLUe5Y4gB246TKGhp9r1DFX vOVQfs1/ExC2oxV+d8iG8JmWU6J4589louqZTAWA03yGhuhqibFUCOqgOkR9aw6br6Ii ISKw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=mime-version:content-transfer-encoding:content-language :accept-language:in-reply-to:references:message-id:date:thread-index :thread-topic:subject:cc:to:from:ironport-phdr :arc-authentication-results; bh=PCNv/0cofB17y2SVvEawJQYBq4Kg6YGte+PBM8hhPQ0=; b=Mza4p1a0dxK174G3rFJbeaf+SYn6D/HL56xo0yGT34w2byh3MmHsa9dQ/ATAXtgS8F wHzo2YCD6WXPUaLtxoCMo4jDhgpz+ffahvvQsk5vur9ZBFNP8HdDAWZyI8vA9AfEUgIR 1bNJMxBOBbj8NHk76cr9yXYa/iW/KLygq2Wj/fNQjwJK5N8axMoFWIstIJJTsm6L8Tkm 5tLE7aZAWsp7wwp1xTPhd0NYmNlpifeXUvb6XQKUNzHPMK2I0oPJ5fjh1MuN158qPsST h2pRT/8uKOcyTh4KxOZ9i5kcPpXHdyz9StctvttVnM+cNFnE3Hk/3CcAVAevgiX7Uc7o RU/A== ARC-Authentication-Results: i=1; gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=uqam.ca Received: from data.hamecon.telecom.uqam.ca (mail2.uqam.ca. [132.208.246.165]) by gmr-mx.google.com with ESMTP id m69-v6si75969ita.0.2018.07.20.08.17.21 for ; Fri, 20 Jul 2018 08:17:22 -0700 (PDT) Received-SPF: pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.165 as permitted sender) client-ip=132.208.246.165; Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of joyal.andre@uqam.ca) identity=mailfrom; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal.andre@uqam.ca"; x-sender="joyal.andre@uqam.ca"; x-conformance=spf_only Received-SPF: None (data2.hamecon.telecom.uqam.ca: no sender authenticity information available from domain of postmaster@MISSIVE.gst.uqam.ca) identity=helo; client-ip=132.208.246.209; receiver=data2.hamecon.telecom.uqam.ca; envelope-from="joyal.andre@uqam.ca"; x-sender="postmaster@MISSIVE.gst.uqam.ca"; x-conformance=spf_only IronPort-PHdr: =?us-ascii?q?9a23=3AwMlHiBx3hdj3b8jXCy+O8D09IxM/srCxBTY7r58u?= =?us-ascii?q?irZAaKOmrsb/JUXao/5k3geQANfrrslcgu+TiJjOHGwN5ZHb6SInUad3diEoz8?= =?us-ascii?q?oNg0o9GceAT0byfqbn?= X-Cloudmark-SP-Filtered: true X-Cloudmark-SP-Result: =?us-ascii?q?v=3D2=2E1_cv=3DGNOoar5K_c=3D1_sm=3D2_tr?= =?us-ascii?q?=3D0_a=3DzdVg5ADNf/sAC0uRWyjItQ=3D=3D=3A17?= =?us-ascii?q?_a=3Dj5JBcSii4TcA=3A10_a=3D8nJEP1OIZ-IA=3A10_a=3DR9QF1RCXAYgA?= =?us-ascii?q?=3A10_a=3D4RBUngkUAAAA=3A8?= =?us-ascii?q?_a=3DEWPDJS0nAAAA=3A8_a=3D1XWaLZrsAAAA=3A8_a=3DrXWxeoHxe1hCXQp?= =?us-ascii?q?iz-8A=3A9?= =?us-ascii?q?_a=3DwPNLvfGTeEIA=3A10_a=3DqJcnUnNV4j4A=3A10_a=3D=5FsbA2Q-Kp09?= =?us-ascii?q?kWB8D3iXc=3A22?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A2CUAQAR/FFb/9H20IRcDgsBAQEBAQEBA?= =?us-ascii?q?QEBAQEHAQEBAQGDTWNtEigKg26WRZVQgRADUwsYBwwBhEACgwwZBjoUAQIBAQI?= =?us-ascii?q?BAQEBbRwMhTYBAQEETisQAgEIDQQEAQEBCiQxAR0IAgQBBwYBBAEHFQSDAIF/D?= =?us-ascii?q?6wSGoo4ixiBEYMRgxkCgS0BEgEhBYMrgiQChV6HOoxUBwKGEYVdhUqGKwOFPIp?= =?us-ascii?q?Ch1+BWCEzLnGEKQmFeIUUhQQ6bxBqAQEZiXWBHwGBGgEB?= X-IPAS-Result: =?us-ascii?q?A2CUAQAR/FFb/9H20IRcDgsBAQEBAQEBAQEBAQEHAQEBAQG?= =?us-ascii?q?DTWNtEigKg26WRZVQgRADUwsYBwwBhEACgwwZBjoUAQIBAQIBAQEBbRwMhTYBA?= =?us-ascii?q?QEETisQAgEIDQQEAQEBCiQxAR0IAgQBBwYBBAEHFQSDAIF/D6wSGoo4ixiBEYM?= =?us-ascii?q?RgxkCgS0BEgEhBYMrgiQChV6HOoxUBwKGEYVdhUqGKwOFPIpCh1+BWCEzLnGEK?= =?us-ascii?q?QmFeIUUhQQ6bxBqAQEZiXWBHwGBGgEB?= X-IronPort-AV: E=Sophos;i="5.51,380,1526356800"; d="scan'208";a="258225026" Received: from unknown (HELO MISSIVE.gst.uqam.ca) ([132.208.246.209]) by data2.hamecon.telecom.uqam.ca with ESMTP/TLS/AES256-SHA; 20 Jul 2018 11:17:20 -0400 Received: from PLI.gst.uqam.ca ([169.254.3.166]) by MISSIVE.gst.uqam.ca ([169.254.4.63]) with mapi id 14.02.0387.000; Fri, 20 Jul 2018 11:17:20 -0400 From: =?iso-8859-1?Q?Joyal=2C_Andr=E9?= To: Michael Shulman , Urs Schreiber CC: Homotopy Type Theory Subject: RE: [HoTT] What is knot in HOTT? Thread-Topic: [HoTT] What is knot in HOTT? Thread-Index: AQHUHx/zBP8o0gxqy0GF9f/ZMFkTLKSWTCGAgAA1SICAAG6cAIABPVqAgAAzjgCAAAOqgIAAE3MA///CLBo= Date: Fri, 20 Jul 2018 15:17:19 +0000 Message-ID: <8C57894C7413F04A98DDF5629FEC90B147A4521B@Pli.gst.uqam.ca> References: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> , In-Reply-To: Accept-Language: en-US, en-CA Content-Language: en-US X-MS-Has-Attach: X-MS-TNEF-Correlator: x-originating-ip: [132.208.216.80] Content-Type: text/plain; charset="UTF-8" MIME-Version: 1.0 X-Original-Sender: joyal.andre@uqam.ca X-Original-Authentication-Results: gmr-mx.google.com; spf=pass (google.com: domain of joyal.andre@uqam.ca designates 132.208.246.165 as permitted sender) smtp.mailfrom=JOYAL.ANDRE@uqam.ca; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=uqam.ca 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: , Of course, braids, knots and tangles can be constructed algebraically using braided monoidal categories. ________________________________________ From: homotopytypetheory@googlegroups.com [homotopytypetheory@googlegroups.com] on behalf of Michael Shulman [shulman@sandiego.edu] Sent: Friday, July 20, 2018 10:54 AM To: Urs Schreiber Cc: Homotopy Type Theory Subject: Re: [HoTT] What is knot in HOTT? It seems to me that especially if we want to construct *particular* knots, we would need the smooth reals to at least be a ring and probably to support trigonometric functions. On Fri, Jul 20, 2018 at 6:45 AM, 'Urs Schreiber' via Homotopy Type Theory wrote: >> Once we have the "smooth real numbers", wouldn't we just define S^1 >> and S^3 in terms of them as usual? Or are you saying that the problem >> is in characterizing the smooth reals inside differential cohesion? > > Yes. > > Possibly one could make progress by declaring shape to be homotopy > localization at some type A^1 of which we only demand that it be > homogeneous (as in Def. 4.8 in arxiv.org/abs/1806.05966) and then > focus attention on A^n-manifolds (as in Def. 7.1). > > One could maybe declare that a smooth n-sphere to be an A^n-manifold > whose shape is equivalent to Disc(S^n). Classically, this should work > away from dimensions in which there are exotic spheres, hence in > particular for the case n <= 3 of relevance in knot theory. > > Best wishes, > urs > > -- > 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. -- 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.