From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBDWO5HFG6EDBBGNBZDNAKGQEPPBQWQI@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-it0-x23b.google.com (mail-it0-x23b.google.com [IPv6:2607:f8b0:4001:c0b::23b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 1fb569fb for ; Fri, 20 Jul 2018 16:40:58 +0000 (UTC) Received: by mail-it0-x23b.google.com with SMTP id p21-v6sf9564005itc.7 for ; Fri, 20 Jul 2018 09:40:58 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532104857; cv=pass; d=google.com; s=arc-20160816; b=HUIOkIHGXA1HEaSDyJNpvhJPvOw3OK/Vf4IVHRRUvTrnuxwEiDkZ1+n+en5t9Y0THJ kISGYXp2N9dMINmtfobY/171QdEH7xOf4FWMICK5QNiptBG6cA+OxOOdIqsBLkgAS5bS rDmf4Gc8PykJzD7i/kJOkSf9DFOUJXrWVfQBGL6y7wJvTvQ5HtZgLjRwvedvdoxLZk38 Isk48OrV9NgvIVObN8h9DIbhofMKxJ1M7YWXdehAPI2PPpulelxG1hCz94GbY6CgzOuF sxtlz5rCJYyTZFYJfW95VD8k4c43XELPrKfLOggXV0KOwbARcMdhNUlz3YyoEdJVWN4f M32w== 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=Ta6szy4wMEhtOy0IcFNRFd/4RO3yFQh+XjlUOlj+EhQ=; b=kMOE86OUzjL7pVpHLZoHGJEwCSTBNHlPwpkc0mHBPIP8jtbdpsoN6VyurGUj6IpHj/ id7R4lPX/WMh5qph3Ei5xYxIW/dpjCpGrX5eYF5TtlgZHOfc+WetWnjBOBX3W8QTRIWR twOP9p7KyY3/eGR116Cj+NefTclkOmw06cS1bvHGT4UgQrNElZuRchp9yp5l43NpkHqo HNynwHLsYwB+QyPQiRrJEH95QW7zEcBHRbgCVWOJ+l41CP6CxlGTSWRcJ6f0JaRS6LuE YB7PD1krSNzdXc07ssinFzvuKBoF7NIVclyFmsLY0JHlrWE8wrjBWU1KKxsnbYBAvtRr F0hw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b=NOYuysxa; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::42e 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=Ta6szy4wMEhtOy0IcFNRFd/4RO3yFQh+XjlUOlj+EhQ=; b=Zj3v4c4iQok6VQMcxZoMdBu+nPgJGCW1cniV9eo/EyQQ/kT2Ub8vbBQDdLvRKXnCCP zqoMgLty40K9aR50/ZmnySlwnfWG/Ki6tadxdFNq21QmOCWdFHxtVrJkpHmq/xM35ogL COc4dCka4gWYIEK2nY82amFQS/d06z3+Gc6nnOhwK9bo7/Zw9kYCLA74/9Q4afI9Ekw1 iBn5AUrMeBScjnBQ8b0qRmqGN0CknVkRUNeeIHtapsVuGtCuavdzT/qn9X6ncES+Aa4i sY89nylFecfFx78Z3CB8Z84H3kaFXbTaAKUE0Hxgbjk5lGLn0RjG+cKh/RA/rAo+CZ2x B5+A== 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=Ta6szy4wMEhtOy0IcFNRFd/4RO3yFQh+XjlUOlj+EhQ=; b=ftrHprJypsAq/+klz+8+mTeqgJVSNzeh0yWSXQQdJPsJM9cL9aSfxyDcIGwWzafXC4 t67jRYtv6nMi7KDQ8EiDiGadc5+YqqfNaEVMAIukEoU/LZUwZ+H/rpen+BsaDVZicz14 XzF5m5ZI6rL8JQ7E0bBzlUPTSWPm5FCPBZeCF0n9MWIk2ib4nhdVUj7bri4ndqUKVz2p M8gGkPNkyMh+/ck2Epm72IfvYwYS7XHrcy3CmXoBDu8ujm8SZU6ejThmGVNcQaHT6B01 VErVB98bIR+M6ZErdqzRgU5/YWXemRXxiTz8ssZGzrPtCFcVpRhY0HEmtJsedKhdl8fv hiCQ== X-Gm-Message-State: AOUpUlGHe5e2ddddhhEuLFENXP5ktrdObCfpgj89zigMQ1naNU3MCmxO 9uTItkaRh90pQJu5zHG2u6o= X-Google-Smtp-Source: AAOMgpdFz1drCvU9jgYVIIdBPL0dD4LONMuiJlV118N6wy8j3LQ86/m/GOAZT+gLHUOlF+O8RPZh6A== X-Received: by 2002:a24:4547:: with SMTP id y68-v6mr16489ita.1.1532104857278; Fri, 20 Jul 2018 09:40:57 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:b719:: with SMTP id h25-v6ls369345itf.10.gmail; Fri, 20 Jul 2018 09:40:57 -0700 (PDT) X-Received: by 2002:a24:27c8:: with SMTP id g191-v6mr1317596ita.20.1532104857032; Fri, 20 Jul 2018 09:40:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532104857; cv=none; d=google.com; s=arc-20160816; b=oL/oUdcBPoSIOl8ESiwIY7eXZpxlGDXAHWkceLDSAa8XfqRMJjsaZxGI5QI4muWY/P ws02Mqk1P/ntecq8ouQ1Qy5flL26BngrpzjRuIu5Tr3y0HxEr+PS4Pa3418Csw77Cb9e QbjJ2xzC9TVbuPqeKFhPpuUAptUyeJrxQiQTfw/5FTkGwtO7nUnt6M8SaPXUjVzS2C6A pY/hSvxTdL/lQrYjiA3nqnXeVCvLBMI2Neev77qX2BI6/fHN1X1ds84f0hHzH4AYFXZO HjlV/48WQRv7FATcJqWru1WZJW6oj/HE87QM60ItgKIcDEfzTZPzLo0na0Ecx/Mp4s49 nP0A== 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=HS2WdTF9Z6BMmUCLp7uOPXOds5J/HEpx4RevzyNpaM0=; b=Kd+bPgEAjwR0zTX7RvdjWgPIrxoLkEI6Hpy/lPAGzHisDACpYun0W+JIiHLcJijOWV sLtrzXQzNQP7fkbs+bT50RTet2r/4Ilrl6HvO2K52CIcPUw9B3VLI06p6DdBQjf5Odn+ uTtSVoYXxBfrwIGeVRGHtwBIYUZ/voG7wGXL9D582XpZb1niLRypF2IOD4Wy+L4Aky+9 mXrdPuA+ICJ6hBIZVyY4M9+vlCL60mmxxD6k+f7arh+TpiG+cb791BJAXpHZcLFBKzIQ U2Xb/TZ0oYkNQQe7nGZMDQjsU9MwysDT2Qg6HYleqoG4gtNhflX0f0j1iYlkZ6HEgOgO FR8w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@googlemail.com header.s=20161025 header.b=NOYuysxa; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::42e 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-x42e.google.com (mail-pf1-x42e.google.com. [2607:f8b0:4864:20::42e]) by gmr-mx.google.com with ESMTPS id w131-v6si369139ita.2.2018.07.20.09.40.57 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Fri, 20 Jul 2018 09:40:57 -0700 (PDT) Received-SPF: pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::42e as permitted sender) client-ip=2607:f8b0:4864:20::42e; Received: by mail-pf1-x42e.google.com with SMTP id l9-v6so91774pff.9 for ; Fri, 20 Jul 2018 09:40:56 -0700 (PDT) X-Received: by 2002:a62:5ec3:: with SMTP id s186-v6mr2919426pfb.129.1532104856458; Fri, 20 Jul 2018 09:40:56 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a17:90a:a001:0:0:0:0 with HTTP; Fri, 20 Jul 2018 09:40:56 -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:40:56 +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=NOYuysxa; spf=pass (google.com: domain of urs.schreiber@googlemail.com designates 2607:f8b0:4864:20::42e 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: , > 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.