From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCXZJBXDZ4ORB4OIY7NAKGQEK4AH7PQ@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-vk0-x237.google.com (mail-vk0-x237.google.com [IPv6:2607:f8b0:400c:c05::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b229c522 for ; Fri, 20 Jul 2018 13:32:34 +0000 (UTC) Received: by mail-vk0-x237.google.com with SMTP id e185-v6sf4122169vkf.19 for ; Fri, 20 Jul 2018 06:32:33 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532093553; cv=pass; d=google.com; s=arc-20160816; b=sqJJ3YlR2dwr7TFiWtue8WvZCB9bW5h1/4Rfmx/wbN3LBaQ8wxTt2g4HAnbEXDFNaJ QFVH6qjKHUN02SzsUMB+WfKfFofvHaMsIl3oqd4ooRiU1iCfAc2SiI1G1RrP1zQQHXop N8gxh8YjhDZPoMeOI9iQE7x7d+OFhctCZojLdur8+Ix12sX+wq01LPblXYU3aYvTKlLP eBUx7C5XBjhYDdRq0tE75LitX4W6YzZysMeJ7HwaUqKNOFfbUtVKpPbSVj8d134U9FbZ EAsq2nkLuxQ8K3he/jZHZu71BP9vZNkeag3tY7RxpNgK7nM1NoZ6cDOpAoshqEWLaUOr ey7w== 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 :arc-authentication-results; bh=iPae8sqV5W76m3VW1rmRsbawho5BMjTEvCh8TQRy6Mw=; b=Tn5xDHV8CgNDJQ4PmWeclon2+qkk8M1oyOGV7+d1qP6l/eo26yMranhpeZ2jOY2dVh 1F/SMUL64qsbQyqy6ZQeoXlA/eGq7LwzKQwcHKRsJMmHKIqa3RUqosqZTChLVGQSBjsr 6e4enrHBt3PBvM1r+mczmQEw5wEDGWoL32B44WnK2ktVWnaQkdZw+Z5XApeMVg1WcGpm lWzPVVXZB4RtCnl4G6nDejfCI36O39pDo64rVRPyHKX629Qy0G+pzlj+r0eAVgOxmJcx nNTbF/pRM+Q6MamORJt6eyh0jGdwx59lRhzRaBHjvUhul1jcVYpCV62f3y4HTu2OcnGR Sn6g== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=koZ6N9n3; spf=neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu 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=iPae8sqV5W76m3VW1rmRsbawho5BMjTEvCh8TQRy6Mw=; b=KPFSx7xC6uUdEwdM9osruQcdS8cHog3rrDaSwaaG9rI3mEBieNotAlKj7WvcERzJJG tuH3d81vLTk1ht/P+zbPr1z1SK3fwbZibaKcpteihCohwoFdhwoSy/u/4fnmJxNe9eP8 4MnvpHItxb8spN5cXTeLvoOtjhh8awxryu1OgpJf30qcbkJxps6xf/R5KpEZTEFVmkw1 wW6T0ybg8yyc2DvTfefTGiyR8hRyvHzCVWg6GQUlECebsGDM5uRTXGKAzs6CQfg+aeRL 5+1MCSws/woaC9yf4jsH/OJ4KurKE+3IT1qdl8cE+toDt9r1GCMpW6dpcf9n9KSNCdZ9 Vmgw== 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=iPae8sqV5W76m3VW1rmRsbawho5BMjTEvCh8TQRy6Mw=; b=SL/WAntlQivT86PhgeUwIjfmnl9kACm4AZHNJ7mat8OuhL4qPss1jm7Gv1qOQcXJ88 oB78vBpzmA5aXbywcmOlgxL+dXp9BKP44eJLCdkcPnCqBPOBZ8X8ZjWkgtYLl3l1lkk+ D8zX6zi7NZ1qhFKSNxwjIY4MEG+juEWE6Ywwlns7XdJVCxQRwAldMV1GtLBu9Yd24QXt 3VbTshkFBiZgh3W9BcsUIPuPjalPXTflET75Sqavi7zJPNWPmUs+SzuYUOnmKKP6fS3F TwdBBizOU+NjBaWvSVWvXuuh4EsoY8cZpNFXS0U7QLJ57IJOUTY1sGo6IToPnBCeIWpo 9umQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGNfF0doVVupazuQullxcvP0yMG+9g1Eo+pB98UvrVxKD9IhlWB QfJzQ9tKCue6im8vZKBBBYU= X-Google-Smtp-Source: AAOMgpfC+tDfdNkT+xhQz7GuRz+i3sQaRKf7FhZnznKhPdyihlSrXUUwrpdmX0buipALDN4lAgP2Ag== X-Received: by 2002:a1f:85c6:: with SMTP id h189-v6mr8766vkd.3.1532093553127; Fri, 20 Jul 2018 06:32:33 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1f:2a87:: with SMTP id q129-v6ls130476vkq.12.gmail; Fri, 20 Jul 2018 06:32:32 -0700 (PDT) X-Received: by 2002:a1f:8d4a:: with SMTP id p71-v6mr898719vkd.109.1532093552821; Fri, 20 Jul 2018 06:32:32 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532093552; cv=none; d=google.com; s=arc-20160816; b=le5auSYnxR5kzO5y8EQsk0mc+UzZ4VSTwYezEZOU0TIhC6/4TrE7GCCXUPvpj7HtnP VkS3K7rvf1fDRRXrAypozhGwypeNWjOy39elcppxiE1kpW/+Lociefj4d4LHJWisC1st mU3IC71I11pLyFCC/11Q0mUS23s4yHgtsrPWQu0d1Ml59lyOgRzPT0aWhuiVYcMpB3/f LfAmgz7bbHZN4aL3Qas/N/PSfYRF38P2ejZ7ynprvmlEY+ow0hBKpXAWUsnJrUPKVhuX i7dAWrsUZaIbexReq/PTCwe5OKoLbEF/nDLPDYJcP+kr1blQPiiUkmMtOd7lll07GQ1i G2pg== 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=unfl9dPRRGBLRYPR24qTSaOT0CdEkBavd3Hw8zXj7pU=; b=GjUrpiXTJzBBpVNcF07Uzj7ktn26eg1R/Rbb3DEdI+6STxrhD6pUjfituQp9RbLbLa qZQCMKZSNUL/LnHnJ4GZPheF3kMJBcoGKMR0+R1ZT+QQUeOCkiKdrbH8qakK53Xuly9z 9RdwsSuNu0vLtlcuU1vOUFqtrDbXjKDNStVt5HUjFqFD5Il5OLPQ+s3vsDik7FX98Tqd rrIvv+7SqqDnZ9PfItyKA5GxZAWltYXumorZJ4owd030/fVJOXfZw6jRi+mx2qKAsRea tncpSg03Bn+PFBRpy11F5sIZj1calOeFc29UXcu/XlrFDEvRTqYXhnliOELkKeK1r8Xm IxeQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=koZ6N9n3; spf=neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yw0-x22e.google.com (mail-yw0-x22e.google.com. [2607:f8b0:4002:c05::22e]) by gmr-mx.google.com with ESMTPS id e184-v6si111698vkg.1.2018.07.20.06.32.32 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Jul 2018 06:32:32 -0700 (PDT) Received-SPF: neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by domain of shulman@sandiego.edu) client-ip=2607:f8b0:4002:c05::22e; Received: by mail-yw0-x22e.google.com with SMTP id c135-v6so4348872ywa.0 for ; Fri, 20 Jul 2018 06:32:32 -0700 (PDT) X-Received: by 2002:a81:62d4:: with SMTP id w203-v6mr925894ywb.283.1532093552352; Fri, 20 Jul 2018 06:32:32 -0700 (PDT) Received: from mail-yb0-f169.google.com (mail-yb0-f169.google.com. [209.85.213.169]) by smtp.gmail.com with ESMTPSA id x69-v6sm1588209ywx.105.2018.07.20.06.32.31 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Jul 2018 06:32:31 -0700 (PDT) Received: by mail-yb0-f169.google.com with SMTP id h127-v6so4616079ybg.12 for ; Fri, 20 Jul 2018 06:32:31 -0700 (PDT) X-Received: by 2002:a25:ad48:: with SMTP id l8-v6mr975259ybe.387.1532093551167; Fri, 20 Jul 2018 06:32:31 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a25:4094:0:0:0:0:0 with HTTP; Fri, 20 Jul 2018 06:32:10 -0700 (PDT) In-Reply-To: References: <74a010cb-0bf4-4d16-b72f-bf4eda0510ca@googlegroups.com> From: Michael Shulman Date: Fri, 20 Jul 2018 06:32:10 -0700 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] What is knot in HOTT? To: Urs Schreiber Cc: Homotopy Type Theory Content-Type: text/plain; charset="UTF-8" X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=koZ6N9n3; spf=neutral (google.com: 2607:f8b0:4002:c05::22e is neither permitted nor denied by domain of shulman@sandiego.edu) smtp.mailfrom=shulman@sandiego.edu 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 Fri, Jul 20, 2018 at 3:27 AM, 'Urs Schreiber' via Homotopy Type Theory wrote: > 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. 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? -- 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.