From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDWO5HFG6EDBB3WOY7NAKGQEPQHRXCI@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,T_DKIMWL_WL_MED autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-pg1-x53e.google.com (mail-pg1-x53e.google.com [IPv6:2607:f8b0:4864:20::53e]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 926d2bcf for ; Fri, 20 Jul 2018 13:45:20 +0000 (UTC) Received: by mail-pg1-x53e.google.com with SMTP id y16-v6sf5952465pgv.23 for ; Fri, 20 Jul 2018 06:45:20 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532094319; cv=pass; d=google.com; s=arc-20160816; b=bGSIWm0tbYY1UBU1eyTSocUFTcn/jEO5YjbG8lroA9sZrXPEPizusZiaZ8+KYcEolW /6qlLR1DPGRy0VBx5eJJvM5QiTj9onS3JeXh9pSBv0PG6QAAqMi2H7qkVvg/HWy6CxWS rE14/obeDFxN2FDUaMvCohY3g48f6HQftSy+gSnMd4h8q+sXyjVunOhUfutd71wdtArN /Vp9UweZjH59eHZe/fzzzQ3OHpFJDI87KVLP+W/mJbaHNTlQ9z6tBrNocMZgobkQkEjh r/Qh9vtfKMrjzjgiVTXY7njFPOUkQl741TlaAgUswAOdLWYWtMkPK4Aq1EXsE7st8AFi YO6w== 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:cc:to:subject:message-id:date:from :references:in-reply-to:mime-version:arc-authentication-results :arc-message-signature:dkim-signature:arc-authentication-results; bh=BpR0UXixweZFx3ErNntfexJgebc0seYuFGjpRgXfFQs=; b=MOvhwGn2fFNa4sMRmLWtt+3m7mZpTuY5xjozsGh16h0ZGos6gtpLXfC3DDHOLndJAI F1EqIOsOi3jyJCK8lWNL8A3nIuHlUvinbVwlnLdqPDAv75yPnBObcHaQy6BM4YP4T1a3 8Rd0QJ/8C9f0wb8Ws7dvDb/PCOeXLyO6eatD8ThpzrlVJf3baAbN/pY2TA7fGNbnkBvG sJjR5bYiKtnHJ6nJjct73fCcdZ24rlIJjeZJ83PQS12co39o5MFxrwrdcGw4WbrcYGRI qUG8B3SZ/iv0g8dWN7rHVojSJOOhSl1k5xidp2P9Ar55lxe2VBG0A2YxO46LspG3WGX9 UyGA== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b=SIlNdp4X; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::435 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 :cc:x-original-sender:x-original-authentication-results:reply-to :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=BpR0UXixweZFx3ErNntfexJgebc0seYuFGjpRgXfFQs=; b=kOaeUO+5/IkK8ciOKoXSsoGGRIzhSlOoTkXyRBdcn6MRpPr7TEZU7MtX/LFMp1S7SS q+MeVLumpUoIJt5HIYhc1N9P4LeFt8CF/xyXMjbty0JK8s3kCnmIpcrICuUuIlFQc+MG O1uSkqYW8ArZwNFc2tXbkQp4ossjxs8Bq7xBjC0MM1ismzE/7nUzeif5RwQJTLs38rqQ rTJbhAI1P9T60mhA3zAANaki3Dc7IeOibQhf+7mD4x0NGEz1idwqEXQvlTytDZ+W7ZR1 J6i1FVFxDCVYtUOfGLwap+YZMjWKywC6maeUH6MQUYTcHMyJouRv7cGUHRunFlBxkSan P42Q== 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:cc: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=BpR0UXixweZFx3ErNntfexJgebc0seYuFGjpRgXfFQs=; b=lhO3YLXMLPn6zyOeP0cq6VVfPnuL6gQGXbzlUDzTO+UQ/WDXMN8jAT4iiYJQxAetmJ 9fTulGZkd11lbwbXokfsLcwKpOHd5eGhCkD2Ye/pXU2nWTG/nKfR4/g/DGkCTPAH9NUH o9n3sz01lwBdzjS1ZAoJflXxErTtki9GK9HbEjDb+KDSIqE5bJV8KSjTOgryc6IHxXXC unRqk7QSh7kqQC07MEgnS+hDHJeslFrQPWNn43UBClY0X0LqnWS05K5xSwo/OgXmgq/1 qkga/TnDi3K4Xv+z9UAvE8hYspuysA7dNA0Wwkhf8uNPcaxqUE68+EEf/fg7OOPXPeyk YwSQ== X-Gm-Message-State: AOUpUlHlOunnCXV/ccDcvsN53+wjmx4evVUkXQqx+ub4Nc4z9uwvBXY5 C+SNVFYfnlCxaNG+bum/u1M= X-Google-Smtp-Source: AAOMgpdnZXmdHTCTwJpJIFtM2VHD5hQByNvnsp1IrJ5Sx5aQTOpFYmeAkEtI8waIndkhdTV0J/qnqw== X-Received: by 2002:a17:902:424:: with SMTP id 33-v6mr11574ple.1.1532094319034; Fri, 20 Jul 2018 06:45:19 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a65:6257:: with SMTP id q23-v6ls547549pgv.1.gmail; Fri, 20 Jul 2018 06:45:18 -0700 (PDT) X-Received: by 2002:a65:5c4d:: with SMTP id v13-v6mr487871pgr.49.1532094318625; Fri, 20 Jul 2018 06:45:18 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532094318; cv=none; d=google.com; s=arc-20160816; b=OsV2V6rUBPqE9GKDoUPtO9ntrG8IlsYjhD5vKYk2RLZm8g2u1pPzOTII576WHaYML3 FJGfPNZrbWyZEVSN2Tu3WSnpnb3fxrvM8fprOIUuoyBOjWrJmxrIKXw/uu9WinSGjztA TfV0ASDrUeNNINjqXXTbAN4LJq00WF2R57wC/NFFrNZI69PyrsA1jgZiZU+jOg07OYeC uhDhgDjgmUbFUIH4xBKiD0nbS7Kww2SRDILEQRKTBDRkmFlQqaSnQRmkMJiNGZyJhjvy iWbx7nZ7vv+tgbnVj0/CBCWy58uJhMEd3OxZX2EHrzI3dH7Gc9261jRT7HLwLU/sC+3O mZzQ== 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=GkhB5pxn/s9HVz0HOG66uImNT1omjsfrDLrM1nbloNs=; b=jy2RcFM5aYp0bzUpT/cRdze1qwsJ+LqvPLhNpsi/DtZrTa2OEQHrFWg/07Y/muA834 nSseQhHDmhzhZFD8Z7tc4Jj1QeatvhIsk5EmMGb7Q5Y6/8l1eczwDHoYtQ4Kgen80CyA QgfKb1RCiJwbhMBwP3a1/4JtDPdfryBT7FhNPEM/pYRwPaZ7awAEZPvJBgdK1Ogc1OWA UndJAC+NtNF1ASOitTACKI/F04gfncgtJElAgvmeHSDQfORF2BSRwIXiyGaQTE/suKvu lhikiMpupwyOrKmzQnqDHvZckZNQoVRgyctDR5L2XiB2BN2SH555GCHeH/ciJvqqE0Du Cizw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b=SIlNdp4X; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::435 as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com Received: from mail-pf1-x435.google.com (mail-pf1-x435.google.com. [2607:f8b0:4864:20::435]) by gmr-mx.google.com with ESMTPS id e9-v6si102830pfn.2.2018.07.20.06.45.18 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Jul 2018 06:45:18 -0700 (PDT) Received-SPF: pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::435 as permitted sender) client-ip=2607:f8b0:4864:20::435; Received: by mail-pf1-x435.google.com with SMTP id u24-v6so72848pfn.13 for ; Fri, 20 Jul 2018 06:45:18 -0700 (PDT) X-Received: by 2002:a63:9b19:: with SMTP id r25-v6mr2191830pgd.44.1532094318424; Fri, 20 Jul 2018 06:45:18 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a17:90a:a001:0:0:0:0 with HTTP; Fri, 20 Jul 2018 06:45:17 -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 17:45:17 +0400 Message-ID: Subject: Re: [HoTT] What is knot in HOTT? To: Michael Shulman Cc: 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=SIlNdp4X; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::435 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: , > 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.