From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCR3VC42QYFBBOVVYPNAKGQE6AZQVOY@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.6 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,FREEMAIL_FORGED_FROMDOMAIN,FREEMAIL_FROM, HEADER_FROM_DIFFERENT_DOMAINS,HTML_MESSAGE,MAILING_LIST_MULTI, RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.1 Received: from mail-wm0-x238.google.com (mail-wm0-x238.google.com [IPv6:2a00:1450:400c:c09::238]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id b1cefc2c for ; Thu, 19 Jul 2018 18:38:51 +0000 (UTC) Received: by mail-wm0-x238.google.com with SMTP id w21-v6sf2697086wmc.4 for ; Thu, 19 Jul 2018 11:38:51 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532025531; cv=pass; d=google.com; s=arc-20160816; b=0LSGJVYQjernPqXMDuw+JDtd9izNj5RRexb8xzQ9PdeMjoSC8vGiGB16To40xxmyBF YKeYTnRNAXH1SXB1YxDOXFa/502pKxJHRi2HTUDyjVwoMTQqXEAgj4A6IU1kBK56dqfI 1vzy5aSy0m5Lh7WqfDiEB/RP6Y8eQsRiRsF//iCcmpjJRFzUcXMhBWFhwWx8Qq41IQLP iPJVDe7YeN96WFm++0Kl3kgHgMR7ioOjItVKrALfTSV98jYtP4OWD8TgmWcqkun2+7O5 plJLW5Kci/XkIRyUc9wV0op5nUaCtLtf4/Lu2w0x/QRGfSZuqdwtxuDmeF7oHKrKitdn Q2EA== 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:dkim-signature :arc-authentication-results; bh=6sHh+5YPBFBVTEZTZ/25AhUIb6mrecCjNlcofTFRBNg=; b=dVueEkCiVMoS830lcADhEII96Obktxf0AUEkRF0C6Sxm7fE2oq/9VDHhc3+RuNz91T gjWDc3Dn6ltRYpCmhqH/ZpT4NOnXNnc26dMXycok4QBHTHqJrUFcohduFame+c9vV8PL IeTF9oOLNDHxnbaUOHZVews7WPX0o3sjCgDZxMXNHpQszCxkQ/pi5LnWlvuhDTBLGFHP mZLbdmNnTpBbnZjP/YrR0qauan/AlK50fLPxmdkZUunrtWV2lGAQy8bNk5oH+0JVJ4Yw NIrFFwOcoRCjPoq1YVdiI26T/CJqa47NyHPh0Pu/n3a1/Bx1M5x01SAwnbd5uH+2hPv8 sRrw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RHxlL5qP; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:400c:c09::241 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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=6sHh+5YPBFBVTEZTZ/25AhUIb6mrecCjNlcofTFRBNg=; b=MZ3Lk6vCvrJcYG5yo3Dx5pcx8nq7Fh9vV+3OiL/Ua8O1RMyx8OkzKBYTmr1Jo9OeQe gjPiasxDvVSmOAfdeJoe1btG2neqJWkriSfGG/g6v7S2bEeLN6Ubxwks+4iWXqf8XHZW 6hObEEB9VFCp4NwmT2b3oP1lv3lXWbwuYUZ+WCx6rqTS2JMcMSk+d7Yct+bn1VwXQc5L 4ePZjsrhDplaCoMhF+o+yN/BGZxJmuU5btZ3EolwUfL/rEUvPzeK67WjQ24GEqmMMcRX W9kwHJdwDUHV+9GFwHTp9XzTVcEU8MzMxzvEEf881CJWBUaaa2hs1uy62xlNzxWAnW6K RLcA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=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=6sHh+5YPBFBVTEZTZ/25AhUIb6mrecCjNlcofTFRBNg=; b=Y6riwtsda4aFMCqFJ0DQUZ3n49qGKVFaKJfe1oNVxBZpeIzfTO39KEqOsSrQDW3XFh bh/IiLoyyOn/BFTaFNn3awh1Lt1ItDZvElGj7tEYqGPkYqGyyOZSE347liraSiqcSLd9 9whcTyHZ6343a1Syenq9C1c25R/BKiBmDoPKnEmXEJRtxfq3k6qSwqiVS/Ux5ZViPC5+ lnfh2mnZQQk30/m3CdsWj+4OjnxfNZNwH5YrUP4IEgveG1NI4ui44YH1acKELFb4YUdS IndRvy2YaBDRZXi5vGRuxoNYlyBfupCrgSHc5VVBgT+Mwp989KXQvD6Fb1+wAWPcvejL /6pQ== 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=6sHh+5YPBFBVTEZTZ/25AhUIb6mrecCjNlcofTFRBNg=; b=J2Mqbs2Hm7XFv0tZpfE/It0UcW1NhiWChXxgMBeM4L1yoieZb3w9isxsTbQWbHqQ+r C1HNGbSwYKGTsMCk2a2SsVdoTyNsIKF8kxEX3oVYTh94trTA+6FrPvKqx4d+pWt+5iOG FkW4EaL+G8cudrxeQ1Sc81e1y065iWjf5zywc/wYza0tDONtpbK+Gf1w3mbVCSJ09kHJ 2fYgTI4aOynTm5EmzNqlVi2QXJvCtXtUxqTzTjqJLoZdfnkO0z7fyKjio/lKApFAG7Y0 YgV19SX7Kodoc2i3Vz7VwlQaZ6iV3YMKginfI4DOlVX0Za1Jzy6HPHauHwbn6LP2rRvM CrMw== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlGNTVdLObmuhDRBvsM3jaf0yyX+NiHSRxuQ25L4y1mgFZq5egpQ QFWh0y403a/aTkVhYhRAW6I= X-Google-Smtp-Source: AAOMgpdjALMrkcV3N9ng7PzpYJRz3IYSqBATm6sT9GT9G+9MsnjkDcUSbT+zAHOBnoQgfXqBvARmQQ== X-Received: by 2002:a5d:4343:: with SMTP id u3-v6mr130935wrr.5.1532025531027; Thu, 19 Jul 2018 11:38:51 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a1c:8e95:: with SMTP id q143-v6ls51755wmd.6.canary-gmail; Thu, 19 Jul 2018 11:38:50 -0700 (PDT) X-Received: by 2002:a1c:6c0c:: with SMTP id h12-v6mr673732wmc.21.1532025530461; Thu, 19 Jul 2018 11:38:50 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532025530; cv=none; d=google.com; s=arc-20160816; b=xsxKkrf3V9BWj4XIR72MeGSvOYGuHhy+P9rWHDaWaKQfQysBQyBv+5/BRnBSnI8Tmj zDc+Mxq7qNd/96OZC++W1YglbQyP/1HpIiP8I7RDkBbRjBF47Dlf26w9WKsquL2pcAB3 +tEwa4at7AHBA+qu+hfIl0Yky7MxWCP7Z1/s6XJFpQTetwEiyunH85v02Dyp6ENIZu39 SCSU3Qym3pod7A7jAZUu+NrCu/2yLlp3s6TVUQsCUTi2OoOpQdokvPzYv7PnRffm6nNF MJslO98i9L9IdzdSsQX8H0qgaYgLvKZMNzQmRqlfsE5PP9qcAiLM0LtyQU5gVK7HFqVA ryFw== 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=qalGRzOx88ArBvs+3zLTo2g2PpgCGJnUxnrEtq1auFc=; b=f1NfjeeD3EXCjvjOppx/xMI91PnIlt9c3wSx+5nPe+kioYNfePZ9PbVRI5dyKNXshB 7Oh9UdFyIyTrvEhSS78P/llcY+N8br0Nbm41SSD5jZVjMBmgn4HgvzYKIRLQ/tPpC3qW BIXGaRjh6aRy6KZkxponVw7ohQrYg6OrN/JHXbU4vSmZxJ6SfFQ46RRZG/zAzEBdycR7 GB8EOlbDinp0c4EIlvNi8s0l30SPaI4B8Bz9hXn5RELIPFQ4rVVGB69oma+AanAABOdt fgK9lYKIBFfho6KpfgFr1DjYbH1z2hhYzkFgc1hKZd9Qf0LOmm5u3P+RSmqzXvFJkOAO OL5Q== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RHxlL5qP; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:400c:c09::241 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-wm0-x241.google.com (mail-wm0-x241.google.com. [2a00:1450:400c:c09::241]) by gmr-mx.google.com with ESMTPS id t12-v6si190341wrn.3.2018.07.19.11.38.50 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Jul 2018 11:38:50 -0700 (PDT) Received-SPF: pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:400c:c09::241 as permitted sender) client-ip=2a00:1450:400c:c09::241; Received: by mail-wm0-x241.google.com with SMTP id z13-v6so7379295wma.5 for ; Thu, 19 Jul 2018 11:38:50 -0700 (PDT) X-Received: by 2002:a1c:3282:: with SMTP id y124-v6mr5032818wmy.11.1532025530131; Thu, 19 Jul 2018 11:38:50 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:adf:9a8f:0:0:0:0:0 with HTTP; Thu, 19 Jul 2018 11:38:49 -0700 (PDT) In-Reply-To: References: From: Egbert Rijke Date: Thu, 19 Jul 2018 14:38:49 -0400 Message-ID: Subject: Re: [HoTT] What is knot in HOTT? To: "Daniel R. Grayson" Cc: Homotopy Type Theory Content-Type: multipart/alternative; boundary="00000000000082a95d05715e7d34" X-Original-Sender: E.M.Rijke@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=RHxlL5qP; spf=pass (google.com: domain of e.m.rijke@gmail.com designates 2a00:1450:400c:c09::241 as permitted sender) smtp.mailfrom=e.m.rijke@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com 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: , --00000000000082a95d05715e7d34 Content-Type: text/plain; charset="UTF-8" Just for the record, a trivial but nice observation: the unknot is the representation of S3 as the join of S1 with itself: p2 S1 x S1 ------> S1 | | | p1 | V V S1 ---------> S3 Unfortunately, no-one has studied SL(2,R) and SL(2,Z) in HoTT yet. Although a trival way to obtain them is through cohesive HoTT would be nice if it were possible to define these spaces directly as higher inductive types. Best, Egbert On Thu, Jul 19, 2018 at 1:56 PM, Daniel R. Grayson < danielrichardgrayson@gmail.com> wrote: > Quillen identified the complement of the trefoil knot with > SL(2,R)/SL(2,Z), and the proof is > on page 84 of Milnor's book "Introduction to algebraic K-theory". > > -- > 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. > -- egbertrijke.com -- 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. --00000000000082a95d05715e7d34 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Just for the record, a trivial but nice observation: = the unknot is the representation of S3 as the join of S1 with itself:
=

=C2=A0=C2=A0=C2=A0= =C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 p2
S1 x S1 ------> S1
=C2=A0=C2=A0 |=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 |
=C2=A0=C2=A0 | p1=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2= =A0 |
=C2=A0=C2=A0 V=C2= =A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 V
=C2=A0 S1 ---------> S3

Unfortunately, no-one has studied SL(2,R) and SL(2,Z) in HoTT = yet. Although a trival way to obtain them is through cohesive HoTT would be= nice if it were possible to define these spaces directly as higher inducti= ve types.

Best,
Egbert
=

On Thu, Jul 19, 2018 at 1:56 PM, Daniel R. Grayson <= danielr= ichardgrayson@gmail.com> wrote:
Quillen identified the complement of the trefoil knot= with SL(2,R)/SL(2,Z), and the proof is
on page 84 of Milnor's book= "Introduction to algebraic K-theory".

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com.=
For more options, visit https://groups.google.com/d/optout.



--
egbertrijke.com

--
You received this message because you are subscribed to the Google Groups &= quot;Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to = HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit http= s://groups.google.com/d/optout.
--00000000000082a95d05715e7d34--