From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCHZRD56UYLBB2O6YPNAKGQEDD34ZJA@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-io0-x237.google.com (mail-io0-x237.google.com [IPv6:2607:f8b0:4001:c06::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id befbd469 for ; Thu, 19 Jul 2018 20:07:07 +0000 (UTC) Received: by mail-io0-x237.google.com with SMTP id s14-v6sf6779580ioc.0 for ; Thu, 19 Jul 2018 13:07:07 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1532030825; cv=pass; d=google.com; s=arc-20160816; b=JGWzGS5Q9pk93EWTtjKDDYn6JXsQd2upDCQKb/NQJ7C1r801uY+jxTPI7l7a5EA8+D e2QkLox5DLvicl8tHaa33hfeP6eEgx7QSULqZ+b5aD7ZiYeW4kd2314Xo5qdj2lbSN4v QIbPSwdwavBI6ieVoBjfFaFFPYRiAai7fDXQGObxYdgK99EMqv0xbObx46TFO69+F8Io dcxH5CVFH+H1JZlsqrzN2qi6HIeUGkwf3Fh1VExKbSohsBVehUSaXdaPwhxxCKdITAAj raOXVnlVxtjtOKqv30qao1SFcrpCiq6ClE71vsOHTPVam40zQwGOD3Zbpw+Mf+nyRDMg NH1A== 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:to:in-reply-to:references:subject :message-id:date:mime-version:from:content-transfer-encoding :arc-authentication-results:arc-message-signature:sender :dkim-signature:dkim-signature:arc-authentication-results; bh=PEI0lSphJVuccSOEpAGmn1EvS56b9G85w36HJzP56qg=; b=R9+3wQtNMYxqukjHtELBbZzsAFp4s5Pb44WOXlnFU5tQ1z+0MN5uwTyZ7f0VVCbrwc be1BTKlzvOqYymMoCb2QUykK8Q1vEGLpzBpLN+eELkA+M4AsLTNOx6E8nbZHpJwZZfGu u3B1ScExr6lvFIqbTIOFVk25ayxph6LDy2qQTUE6kLQBxO+vPQVg/MtokdaICA1ZMPe0 uGQ5/UXyCo8MviwPGwS5GeEJLSj3seiYU7S8VZcTcjgbHVp4ZBjvSyFNCCbf/Xrt8FuX fusOlwu0d5Pug7CPi2fnIEMJl5t6bqFhPh2cBpqEC797ULtfFJLn5q0zavm1A+MIRVyy QDTg== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=BoGMJszo; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:400d:c0d::22c as permitted sender) smtp.mailfrom=josephcmac@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:content-transfer-encoding:from:mime-version:date:message-id :subject:references:in-reply-to:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=PEI0lSphJVuccSOEpAGmn1EvS56b9G85w36HJzP56qg=; b=DAsbl1yWnyIJEIYbrRPeRc08RdBGXU+HZy9uGY9bnZcmQJDpHeBFGJAnjnSb5ry+Vm lzg2Ai9CsEm0NDnZ5N754csdvkT85CntPsMOrf+owWQmSftK+nTaCbeC206s3VpeDeJD JJXlGu/Mnx4tChDbspz9YO6eKTDB1EMHMhDrj9u55YWmdpvpEHzZBXls43b2Ao8y0Q1v yyT4ohAQHcmM64ZDECHB3nEFmqnwLvLEuiafdfiJ4PRMJiwRc6KLREn3/p4YJ+CDsD9A 1GybH2nbSMJbR9F4C79PcKfS2MdLmhycPTAf58tdwYzBNOW+bmypGcDHiNlILq7xzTWX 00lg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=content-transfer-encoding:from:mime-version:date:message-id:subject :references:in-reply-to:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=PEI0lSphJVuccSOEpAGmn1EvS56b9G85w36HJzP56qg=; b=npD93gcHLQOe/lig4GdjmYEb/a8KxJa6SRBvdwP3SOf6zagSTABwEMu1VfhH86fH1d SjTToKlmEpBogug/xfGlWQ2iMBRvFW5wxP65Y3B+q0Qby35xejwtPSRnL4/nDI+nMZ8A wBDgkUE06tC//jiWZjlBYwZIey2uh/3lRl4fZC1pjxBdRaquVvzyewTuz+A278BLYQ0A 0V/vEYDiDN2GDDubN79j09DTdrU1GKiGWcTPE9JzDEFbEDfO2KlbTqdvlsEj2WKDqKmi QkvLVW/J6MS3L5AcJ+v9rVC7SwJCFQ4QBnZhICiMa52Dg6hqtUCpKJh6jK+CGZ4Ht9SB LYHg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:content-transfer-encoding:from :mime-version:date:message-id:subject:references:in-reply-to:to :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=PEI0lSphJVuccSOEpAGmn1EvS56b9G85w36HJzP56qg=; b=PIg4r4ntTeAQqhnUP+XjDyIZDdZXYRP1kFZXHIbvZrPCXMi8g6INn7gnR69PnSaHid u/3FOWmaBxi2XJ1l0XBk6kIw9NrRmhXH0D0iq/S6bGZIxM0+TQrasbFA4YEL7r+gg04Y lNG0NQM8/aP4l6fqBvaa2mGPtY5AG4Zt+/ar9jiq4eIM7qkWzv/RW65J7FCYtHRcQ7SI iuKtxOT7wgaIAHktqXAFnMmNkGyNhpmf76fFJTS4UMrsDMHsEdDMgzIaw46qylfX8rXT LIp0/DR6pdt2gjVZgOCl1pUwTmMU03U36Qfie0cGW+N+mcLWAzB/q6CuW3Nr7ZL7/5pK bWXA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlH3i2BcQHuBIUClot5xv1WbjfCdYRXs3DVXZDskhW91OL8J8qGr UkHpPJVSwyLjN2wnIZHiTM8= X-Google-Smtp-Source: AAOMgpdMAFrJsltOuM4tuaiveM+pLsdh+UmurpKyR1IVB4LjhN4DsL+Nc8SqVsPMCgtH47RT2CPyWw== X-Received: by 2002:a24:478f:: with SMTP id t137-v6mr38470itb.2.1532030825288; Thu, 19 Jul 2018 13:07:05 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a24:39c6:: with SMTP id l189-v6ls95383ita.3.canary-gmail; Thu, 19 Jul 2018 13:07:05 -0700 (PDT) X-Received: by 2002:a24:674f:: with SMTP id u76-v6mr3543729itc.36.1532030825012; Thu, 19 Jul 2018 13:07:05 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1532030824; cv=none; d=google.com; s=arc-20160816; b=s9OUZkE8V1ss7GlQ6EHxFt2pdp+vlyEGiHq/2+ERchT30y3RaMU4nhtf7rWxWUikkK RUzJQhhCwyOiLPWItxy55U92zcA/WDALrf1KbvHxDDCqekhKsJOJPxw2JF4tfpeWyLZz 4/mAi7ONxGGsZ7PMRGMh4gtChjJuCUtlQ95k56otnEZupeodoksGA6RKNw86hXjjaCMr /qGBSknQj5mnlX/aIHl01111lsoFwkf64pK9cuNPv/4bC8VIXQW2OeGX/gbUgmYkXfwZ gyGUmUI9/1UKRXzQKzKtgsSy/cCDPEQm9qA83xgMfXqXPJHeQAC+18NnzMfPv8Zugcp1 Xpdw== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:in-reply-to:references:subject:message-id:date:mime-version:from :content-transfer-encoding:dkim-signature:arc-authentication-results; bh=t7r/8bxvOYhzPb44KqdAL4PFnx8et+S1vV9ym+Zlu7M=; b=mZ3fiOPhhvRqOD/tfcVkNio2tBS6LMdzr5SVnnMqLOeVPTBhd409AkoyiglStULusI vLA0TdKJiNiXHG/hfkCoai/VRpjX+7LPTB3RqtwsaHfi+3P4crlIACLz9UZHRjILqX0N 4fA3j1G7s/kBXjLl2HKd1VfRNcgeSy0lU+PCJB9ztJWG56PwkSIAcOgoXmzFHjGbnz7W 2+GhLpXk9HtpV6TtjJz/zxbB8ObZqUpYBJkQkWCKm2Z/IpOKVWoLFOqePz/0IsgEufhh o7wD79E+EEuRGsO4MTMzgHiRAqWJNE8OoTdmUG/p2EmCCInlIMvfBfYulmj7Cx6bJIy4 0DeQ== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=BoGMJszo; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:400d:c0d::22c as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-qt0-x22c.google.com (mail-qt0-x22c.google.com. [2607:f8b0:400d:c0d::22c]) by gmr-mx.google.com with ESMTPS id z2-v6si93236iti.3.2018.07.19.13.07.04 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Jul 2018 13:07:04 -0700 (PDT) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:400d:c0d::22c as permitted sender) client-ip=2607:f8b0:400d:c0d::22c; Received: by mail-qt0-x22c.google.com with SMTP id d4-v6so8351201qtn.13 for ; Thu, 19 Jul 2018 13:07:04 -0700 (PDT) X-Received: by 2002:a0c:8af5:: with SMTP id 50-v6mr12187469qvw.219.1532030824594; Thu, 19 Jul 2018 13:07:04 -0700 (PDT) Received: from ?IPv6:2605:8d80:506:cc78:80ae:3bd2:9161:a354? ([2605:8d80:506:cc78:80ae:3bd2:9161:a354]) by smtp.gmail.com with ESMTPSA id b62-v6sm34645qkj.48.2018.07.19.13.07.03 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Thu, 19 Jul 2018 13:07:04 -0700 (PDT) Content-Transfer-Encoding: 7bit Content-Type: multipart/alternative; boundary=Apple-Mail-2DC7B5F7-BBCD-4992-A92C-3FCE0D422EBF From: =?utf-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Mime-Version: 1.0 (1.0) Date: Thu, 19 Jul 2018 16:07:02 -0400 Message-Id: <27095D4F-38DE-424C-A085-EADF30C4630F@gmail.com> Subject: Re: [HoTT] What is knot in HOTT? References: In-Reply-To: To: HomotopyTypeTheory@googlegroups.com X-Mailer: iPhone Mail (15F79) X-Original-Sender: josephcmac@gmail.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=BoGMJszo; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:400d:c0d::22c as permitted sender) smtp.mailfrom=josephcmac@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: , --Apple-Mail-2DC7B5F7-BBCD-4992-A92C-3FCE0D422EBF Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Maybe the connection between knots and primes can be stated in terms of SL(= 2,R) and SL(2,Z), because these groups are essential in number theory, e.g.= , modular forms, quadratic forms. Jos=C3=A9 M > On Jul 19, 2018, at 2:38 PM, Egbert Rijke wrote: >=20 > Just for the record, a trivial but nice observation: the unknot is the re= presentation of S3 as the join of S1 with itself: >=20 > p2 > S1 x S1 ------> S1 > | | > | p1 | > V V > S1 ---------> S3 >=20 > Unfortunately, no-one has studied SL(2,R) and SL(2,Z) in HoTT yet. Althou= gh 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. >=20 > Best, > Egbert >=20 >> On Thu, Jul 19, 2018 at 1:56 PM, Daniel R. Grayson 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". >> --=20 >> You received this message because you are subscribed to the Google Group= s "Homotopy Type Theory" group. >> To unsubscribe from this group and stop receiving emails from it, send a= n email to HomotopyTypeTheory+unsubscribe@googlegroups.com. >> For more options, visit https://groups.google.com/d/optout. >=20 >=20 >=20 > --=20 > egbertrijke.com > --=20 > 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. --=20 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 e= mail to HomotopyTypeTheory+unsubscribe@googlegroups.com. For more options, visit https://groups.google.com/d/optout. --Apple-Mail-2DC7B5F7-BBCD-4992-A92C-3FCE0D422EBF Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Maybe the connection between= knots and primes can be stated in terms of SL(2,R) and SL(2,Z), because th= ese groups are essential in number theory, e.g., modular forms, quadratic f= orms.

Jos=C3=A9 M


On Jul 19, 2018, at= 2:38 PM, Egbert Rijke <e.m.rijke= @gmail.com> wrote:

Just for the record, a trivial but nice observation: the u= nknot is the representation of S3 as the join of S1 with itself:
=
    &= nbsp;      p2
S1 x S1 ------> S1
   |       =      |
   | p1         |
   V  =           V
<= font face=3D"monospace,monospace">  S1 ---------> S3

Unfortunately, no-one has studied SL(2,R) and SL(2,Z) in HoTT yet. Alt= hough 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
<= /div>

On Thu= , Jul 19, 2018 at 1:56 PM, Daniel R. Grayson <danielrichardg= rayson@gmail.com> wrote:
Quillen identified the complement of the trefoil knot with S= L(2,R)/SL(2,Z), and the proof is
on page 84 of Milnor's book "Introduct= ion 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 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 "= 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.

--
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.
--Apple-Mail-2DC7B5F7-BBCD-4992-A92C-3FCE0D422EBF--