From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDWO5HFG6EDBBY5BZDNAKGQENXCDFXQ@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-yw0-x240.google.com (mail-yw0-x240.google.com [IPv6:2607:f8b0:4002:c05::240]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 2857b20a for ; Fri, 20 Jul 2018 16:42:12 +0000 (UTC) Received: by mail-yw0-x240.google.com with SMTP id t189-v6sf6643467ywg.2 for ; Fri, 20 Jul 2018 09:42:12 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532104932; cv=pass; d=google.com; s=arc-20160816; b=jNAVLDS5n1qkJ0UkxEk6PG0YbrIijDGlulShUp2v3hhTJA0fhQrJqYhCngSwHk5yjY cOx5jFIHAy8H4pV2JrQ2lfdRrNKAXl1AvUYfi/M23q/Fjez2Ad/8AmtY/LySkwmUGbdO RDos/keMNJnqWBsq7iQ/bYnpJMeHNu1Hlk7/xsuCXXJlkQdyKUS78IZl+pHluPmhGL0A SlErd3wNUpfqMxaz4IqzncIPdQkOqXWIcxhoUnLtH9p8BjlhGYOti30A3m6ffSawD+3g NoOtSjJi7kJZN1WZwUUcTIBIa7SdF0GVvRPaLy/FF0JNXtGizJrkg4bo2WLDsdO86yE4 bZXw== 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=Zm5x6acllNjQSXzjAdvsXfmJNBSeZAiqG6rzxuMcqoI=; b=F83fsQUwjeNjmMxH2TG9+PqhqijhXB40eGPEBaO5LHqtGiM5OcHaQX4mDEEZNSXwSg AYe6EtQ324iCDDVJ/HMhlPRQICLGV25zohYqn+uiqZnmBKHljip6Fp2JjQhEogiugTQ6 GQvk4erSN7sOyyQBtClSDzxsjRU9R1Nm7ELeoZQgK1l+cnfVzqDw/GFQSbr2V5XqXUiO lqnrkwDhfwtRMV/Q1ncyrrG2w9gxrQm29+MhxtG9HDQrTwRaEtxox7TcMyzES+GVbgZl TZ/rJ6eDrvdvYoAJFQ/1d9s2lMhZ8n8SOSj0mxTTvOE4wKWDTB6IZ0gUBBLJm+IDslek mZkw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b=IFbvQILc; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:400e:c01::22b 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=Zm5x6acllNjQSXzjAdvsXfmJNBSeZAiqG6rzxuMcqoI=; b=S3IsRxruAROyRljW4gFWHNd1fXRqH/3mNqf2hLAaa+7eC/44yG9JGTjXoGjdF+Hlam CbY+U7hg2A0iDX8DqGDouIDJceGcybb9dp93c8mbtevHUjvOgqlsyRJBD43xax3VlkI4 sFDvoYRSyC6qEkSebkXCLXA/FxuktQpwxBVdJ4DbPH1nYWQ6JLvDEL8+qUi4UKseqjx0 JJhcdwYBloiwvhBaTyhI7SqJZWeXQf9O5istdjM5okV8JEdG8h4ZPaEsN4Iln+8zZpw8 JQCtO2/TzTvTYTI5HSqCQRvGaudipqKCLsn1iFmPoqa/8WxQqFCLA2bnw0t80IcLZOZF quwQ== 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=Zm5x6acllNjQSXzjAdvsXfmJNBSeZAiqG6rzxuMcqoI=; b=mOD/rizM2ag6NbuP5EL/YVd6Nd8ZfYJg9rQy0+lQg9oJJk+QZznJBSyACmFBdbFeqd Zr7oGq76oy+cxQFKum4WtEa7odnPg5mX7kJDsZ6FBHfCBITAu2A4tc7L7/KgiL+ee17H meM6DWuktqiYc92+fWMSoNBdqfnSfNHYscvCe6AhYY1HizeAYwujHPuQGZJ3SaS6H9AA vqteurclMi0vRpcU3A7SgWqgyVa1oVBYD85fOVt2mWnLXW/+86t9ThB/begRL5d1Y/8p b1fls3Y17a0R+Un5wxLzzVpR9ZQ1nvafvfjD210gSPnAu/AAfynPWcc1WkgTt1F+aem9 Tbpg== X-Gm-Message-State: AOUpUlFDz5oYaW7iT03x3udYR9MXBNFW0ZaFsWLk2QUCQqkxd0QfyVTF jQxZ6NOB/oVmlMOn2aduQDw= X-Google-Smtp-Source: AAOMgpeSz5ySqeV16+YCNjV6+RKGJeKh9Z8ICg8MtqD2ZnyHVGxsgFPCA0mCTegcOQYFFZECtjR4jQ== X-Received: by 2002:a81:78c6:: with SMTP id t189-v6mr72645ywc.7.1532104931988; Fri, 20 Jul 2018 09:42:11 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:4181:: with SMTP id o123-v6ls616154yba.21.gmail; Fri, 20 Jul 2018 09:42:11 -0700 (PDT) X-Received: by 2002:a5b:2c4:: with SMTP id h4-v6mr735298ybp.42.1532104931727; Fri, 20 Jul 2018 09:42:11 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532104931; cv=none; d=google.com; s=arc-20160816; b=VAMHJwFOTmMM0ev1R7PF0/KX0I/2YaYvfYJkbdv/1vK5qXpEG6z2wlRajqa2YUjNPI 4MjHoj0gsoBhwGSs/P3dTDeCPcPLsgVfmsOkIblYKTmQQbaNE5wLAZPHCEICR4xEHj6m ZTIB6hqXXfMZ7O9XADUm/AIFL+FkV75E+aQpxTAu/T6kOXbInYKnsmWpgNDU4U+FTE4l Nl9SAo0cLQsPMSk6kRRcR3vFlzp214HxVQKvlmmtc1yezqsvSUYn42BuZxM1GGORiro2 2TyzBzhQ42gdgh5I6j7BmbPSuO7n163CJBLYiqv5jZBoMbIToktWNMVY3zyWD6CQHfPE P4HQ== 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=p04utRrwhsUaknV5uDehgdTqawXYdT2724TdcsTxCPk=; b=T7RiC/76lTPmq9eiKrRRo1Zaam+wttDLH/FmGRKdyKv1KBi843+OCfsykM/RNbZd6Q J2FHhLgJGv1ZQ9z+Q/8GEy+j2G1bqjOmA2RaNStcRDP2Lc1w/CyIafq1AqQOoTMQfCed ADCnJMtzvGXZkVJ9MZOsl674+2Wa+5P+O49pZcLtFWNdRi1r1DlLz/k34hIdqNTIEF8Q ELD7YApvJ1HqzHHzW8REIsr1YzFfs08EOe0pra9wkZdvS0J7gc2A/XACXAR9OodwXRKW VOZV15B/z4ZNzVinpDZZu3Si3hsdrNU2481UCzxqUFW7vqfsenryKeen3oBaaoxE62NI Xmvg== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b=IFbvQILc; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:400e:c01::22b as permitted sender) smtp.mailfrom=urs.schreiber@googlemail.com; dmarc=pass (p=QUARANTINE sp=QUARANTINE dis=NONE) header.from=googlemail.com Received: from mail-pl0-x22b.google.com (mail-pl0-x22b.google.com. [2607:f8b0:400e:c01::22b]) by gmr-mx.google.com with ESMTPS id g1-v6si110921yba.4.2018.07.20.09.42.11 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Jul 2018 09:42:11 -0700 (PDT) Received-SPF: pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:400e:c01::22b as permitted sender) client-ip=2607:f8b0:400e:c01::22b; Received: by mail-pl0-x22b.google.com with SMTP id 31-v6so5435084plc.4 for ; Fri, 20 Jul 2018 09:42:11 -0700 (PDT) X-Received: by 2002:a17:902:e85:: with SMTP id 5-v6mr2794832plx.318.1532104931021; Fri, 20 Jul 2018 09:42:11 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a17:90a:a001:0:0:0:0 with HTTP; Fri, 20 Jul 2018 09:42:10 -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 20:42:10 +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=IFbvQILc; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:400e:c01::22b 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: , Gr, here I mean "flat" where I wrote "Disc", and the counit should go the other way around... On 7/20/18, Urs Schreiber wrote: >> 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. > > One could require an isomorphism > > Disc(A) = R_{Cauchy} > > such that combined with the counit > > A --> Disc(A) = R_Cauchy > > this respects the homogeneous type structure on both sides (i.e the > postulated one on the left, the canonical one given by addition on the > right). > > To test such choices of axioms, it would be very helpful to have a > concrete proposition in knot theory in mind, which one could aim for. > Preferably some very simple proposition which is still of interest. > > Best, > 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.