From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDWO5HFG6EDBBHPSY3NAKGQENX6RZNQ@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=-1.1 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-oi0-x238.google.com (mail-oi0-x238.google.com [IPv6:2607:f8b0:4003:c06::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id e396284c for ; Fri, 20 Jul 2018 10:27:43 +0000 (UTC) Received: by mail-oi0-x238.google.com with SMTP id m197-v6sf9331882oig.18 for ; Fri, 20 Jul 2018 03:27:42 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532082461; cv=pass; d=google.com; s=arc-20160816; b=ckpeFXLW6QhUd6BrEMJ7v6iw1uyqYqMtnaP+B66/Zp7CK2qH2O/PdaVoAZQfnRLfMu HpG8RriG35CKCDKgcji7OOHKpTnPvprAfAerdVesVGTENjmuOFJJ/9nIRh6vqEaEq5At 2RXjgPrhAOdz4QNygEZ38I+/9AAWtNkTOGyFw/3erzKOuBFwIhsNetNzD01dCUkI4lts UMkUYwZIIO9eLHk8RvF25OS37owKosjlJZsas1Qvxsa7v8QlGEKx15LINL1WArduZlJp R9HhIE3gAI3GTlq4URhZtvZlLDWpHvjbxbHKQ27EgNOszUWT7widxIS/YXHnNpsiAGMY ZzaA== 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:reply-to:to:subject:message-id:date:from :references:in-reply-to:mime-version:arc-authentication-results :arc-message-signature:dkim-signature:arc-authentication-results; bh=/kRBithDqspl0YmRL6LPyjP6vwXkzYAJ0VmCqnE6y6E=; b=RQBbaoF6m/cxURjFtpxP+kTiGv4rUBYTi3x7Q+7QdTlsYLyy4Il8FTb15gqv72IAk6 DFEToA7/pu1ZMKpZxEQw00XseJOw5rak6PJgPqH2f3UozqX9sQy+RBxIDM5i641vPMzC 1o6hcMot5h72YojECDIIF/m4gw5wZWQ1kGcXjI3Eb3536eAbT3iBMsIcADJbAyqOip92 40lGvSc5IdEJcdaYlzHdkD0wVhLq7irrPlJwzhLVBuW8R/pe8fZbNch4aJd3l6iZ5tjy snoQE5gcQFpT1qoSxCojclllGZzTuTSYX5QzmNrtYB3lGN4eeoOh1eaJDhTnAiu0rUXu dtmQ== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b="im1r/UuA"; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::52a as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:reply-to :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=/kRBithDqspl0YmRL6LPyjP6vwXkzYAJ0VmCqnE6y6E=; b=TY+iapdm8P4eqTpvEGrCwO54VUeJRc31vMznnojXJDytri0PXfZ4DFWtTiS4bKkGj5 rQzYjBT7CTcbOYLd8YF5hiM730JcdOvvLYdcQ0F1DvsWemMelrh3yMBrM1sOTOkIDVds 3YHs6zgemW6+0E4vYEb/nLTS9DAY6j2oOXyjKk4UsN4XpIMs8m0x9yIyXvGExTNJV9h7 SZjnOxsLlKkkImZAnuXS1DMUlmpztYVhvDHcoi8ubqa78ao7cYCb/kGZavtXrJXd14b5 GSjrdID39UIM3O+8NT4ViQtgpW9lWbiKg/Wdl7KGXVuLJ9mCMLVjfnQo5v+0igF0yaBu EdAQ== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:x-spam-checked-in-group:list-post:list-help:list-archive :list-unsubscribe; bh=/kRBithDqspl0YmRL6LPyjP6vwXkzYAJ0VmCqnE6y6E=; b=aQh3LV+AFQ//A20ZBcjOad904wUvLO5ohxJoW+io6U+YF+xnkjgTvRYGXzvZtZEpMR W/kRWoXh6L8PYW7Vkf/DSUjW2jCmj0mxXYeIEMTrpISR6aqy5rVpRY+DE1gA+T793L62 QRnN/iOfhDb33v1za8fqcBHuRkaNOvVuuMOICRRqlmnmRQ4Fci4DIWHiglgkR0S4xDqt hn/tAo03sXNcu9lvlmpp0I7lQP19KX55+v8wjkGKF2AO7r4FjAGTddr4wN1CGxWZGnm1 OuM8cDPzY8dgOgqi3EoCHvwJQXUEn2S8sgjlMZrdjU8ZEKZfXd1sy6acsDlCCkMLwxb+ 7Z+g== X-Gm-Message-State: AOUpUlGN0ppqn1VZ9zZHhzhut9KRK07qzXbO+bb0D3SkClFFaPoAO7Ng nlXuG/yb/NvfAuMU5AX1bFc= X-Google-Smtp-Source: AAOMgpdeddt922ZHf4+c97pBPNe5akcfivEoPRWDNsnaGCFMhlN2UTQx2MC5ymGfK4MSqpPU/9GuMA== X-Received: by 2002:aca:c744:: with SMTP id x65-v6mr108048oif.2.1532082461252; Fri, 20 Jul 2018 03:27:41 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a54:4388:: with SMTP id u8-v6ls1032703oiv.6.gmail; Fri, 20 Jul 2018 03:27:40 -0700 (PDT) X-Received: by 2002:aca:3cd6:: with SMTP id j205-v6mr779253oia.3.1532082460919; Fri, 20 Jul 2018 03:27:40 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532082460; cv=none; d=google.com; s=arc-20160816; b=d0qcGTvKe9z1aZnpY50vw3luS5aJ230/DIQrf7CUPPTRkV8RZ7PvuSV7JTp3sxoEC4 jMOFg2zsg7+qev7LDpljeazoormS9sAViU42ZQAYUE6bAA6n2e8fPbZcP5ZlmjwkPqbB h8+0WJWkM1vYPHEVtMcCLyZWg841GgVxbGqvE0x8Fhg04zhkMym2EH+dDrTihH5u9QKq GOnXDk2gURYy4hZ/+4dBpgTXa4Z7cBkNkQU7dZiDYJvf4UXK2Y+wYj7RhH1+bDdZabJK tcUS3leXQK3LOnRAh/5Z8M+Or9WMkkpvIGNsE3T/WP6Sqa+HFbpbsKN1sDWDdYuyhUTM 4OXA== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:references:in-reply-to:mime-version :dkim-signature:arc-authentication-results; bh=Uwq1R6oPTaOt4YtxsUNk96e46bUg3oiNJIRIQtxEWEY=; b=U8N8ra5nIWAs3NNpAKSNwNY/XQlVafOMfwyfdoSF7jFD2HsVO79Y9CHfFN5WxJ0imr nIrlwSjHKQ003bbbKG/JuL3mBt6jWrm8n0oRnUvdb4M5+3g9XuVGFSa/tidoBPvCSy2Q Ro93PPby8SMD7YvJGS89LtII9GoTAKOq73ZgV/Sjf7bG15YEs0rmjASoa1fyQRiiLOSO GWwg+r9Bl2kzEHWpokZtvG0dQN4AaWc1kUpvzbpummDK1CcIJxigd8DDc1QalYSJEZaG OBvOibgQD55JcbZoLGVDokPy4K1KJO5afCLlURJBswZaEROvVVTveT0Ppj3b6bsaQ4BG 3rpw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b="im1r/UuA"; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::52a as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com Received: from mail-pg1-x52a.google.com (mail-pg1-x52a.google.com. [2607:f8b0:4864:20::52a]) by gmr-mx.google.com with ESMTPS id 2-v6si80723oiq.0.2018.07.20.03.27.40 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Jul 2018 03:27:40 -0700 (PDT) Received-SPF: pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::52a as permitted sender) client-ip=2607:f8b0:4864:20::52a; Received: by mail-pg1-x52a.google.com with SMTP id r5-v6so6524514pgv.0 for ; Fri, 20 Jul 2018 03:27:40 -0700 (PDT) X-Received: by 2002:a62:87ce:: with SMTP id i197-v6mr1627689pfe.62.1532082460108; Fri, 20 Jul 2018 03:27:40 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a17:90a:a001:0:0:0:0 with HTTP; Fri, 20 Jul 2018 03:27:39 -0700 (PDT) In-Reply-To: References: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> From: "'Urs Schreiber' via Homotopy Type Theory" Date: Fri, 20 Jul 2018 14:27:39 +0400 Message-ID: Subject: Re: [HoTT] What is knot in HOTT? To: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: urs.schreiber@googlemail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b="im1r/UuA"; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::52a as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com X-Original-From: Urs Schreiber Reply-To: Urs Schreiber 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: , On 7/19/18, Michael Shulman wrote: > This does seem like the kind of problem that Cohesive HoTT is designed > to solve. Indeed, or rather that "differentially cohesive HoTT" is designed to solve: The space of equivalence classes of knots of shape Sigma(= S^1) in X(=S^3) should be the 0-truncation of the "shape" of the sub-type of the function type Sigma -> X on those that are embeddings of smooth manifolds. We may formalize "smooth manifold" types Sigma, X and "embedding of smooth manifolds" in HoTT using an "infinitesimal shape modality" "Im", as in Felix Wellen's work ncatlab.org/schreiber/show/thesis+Wellen to produce a type (Sigma -> X)_emb Then applying a shape modality to this shape (Sigma -> X)_emb yields a type whose paths should be interpreted as smooth isotopies. Hence the 0-truncation of this type Knot_Sigma(X) := | shape (Sigma -> X)_emb |_0 should be the type of equivalence classes of Sigma-shaped knots in X. This would make sense for any Sigma and X. Indeed, the main problem from this angle seems to be to axiomatize the generic manifold types Sigma and X to behave enough like S^1 and S^3 such that one can draw usual conclusions. Not sure about that. One might be tempted to use Mike's "real cohesion", but that probably does not admit a non-trivial "infinitesimal shape modality" (being based on the topological real line, instead of the smooth one). Incidentally, just yesterday I tentatively started compiling a list with "open problems and further directions in cohesive homotopy theory". Just added a brief item on knot theory there: https://ncatlab.org/schreiber/show/Some+thoughts+on+the+future+of+modal+homotopy+type+theory#KnotTheory Related discussion on the nForum https://nforum.ncatlab.org/discussion/8747/open-problems-in-axiomatic-cohesion/#Item_1 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.