From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: homotopytypetheory+bncBCHZRD56UYLBBLN6YDNAKGQEG7QD4JI@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-qt0-x239.google.com (mail-qt0-x239.google.com [IPv6:2607:f8b0:400d:c0d::239]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 33091eed for ; Thu, 19 Jul 2018 05:18:39 +0000 (UTC) Received: by mail-qt0-x239.google.com with SMTP id o18-v6sf4963313qtm.11 for ; Wed, 18 Jul 2018 22:18:39 -0700 (PDT) ARC-Seal: i=2; a=rsa-sha256; t=1531977518; cv=pass; d=google.com; s=arc-20160816; b=JQ9NyL6wpDop6vtpdEZG08UMDSKbqT1hCOGv9d8Yv06VKC1NPbz2wpa8d8cjK60FP7 tp4EDcDNFIpdmV0dOWjs6wqeEFw/oFWf/fWPjZrrveMbi35P1amA5lDyioG4kHDPNvr3 8r2CmAedcGu+b2uWvbUWDz9ufw968LzEaAKaZ3oj9soCKyPYZsk8Pu5VYIJzjiPiI9B4 tK3U737doPG50ylXlMRGCh3kly5+zwcN5S768IyvvEMagftZIhjy82Oo19Z3pWTFkXMC YTSnU+pFs98vWQ1MO/0ZEnZB/dh4wjHm8GPsGdCulscpXvlmwwmDtSSHjLmdtJ1gYIcE aTxQ== 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:subject:message-id:date:from :mime-version:arc-authentication-results:arc-message-signature :sender:dkim-signature:dkim-signature:arc-authentication-results; bh=+FLqqMMBSpJQKZS3r9CdosloQz6czGRgqxHi34Wuhsw=; b=AHWC3pVGa6r/ul+RM3Ymbq2U/34grUvaF8RQ1KzUWsHa1K3JExAThnagiSmzhqsAuE CoxQ74l5hC4B5tAKgNzLzx9ycSw/sQsHoaoG00q9KCQi/FmcD6Tkw7xtOG/+n7EjNx2t an0ZtLxe/uppNO1O9LajjlcUlePYI3Pl1IzwYQFjua7tXBWcXijmb7KhInf6Y9wolqJg +OpaRQPwYhQ6d4OT95X5InmIBd7Iuqd9g2ptD8lzHn10eM2JOfuFW/NIqHwV1TjEISXP yKMQ2ayeM3NKOZXzAa0pWLX3gZzNxrDjQ76UpO5B4y+VAO5FgeWzL328ViAgtmcS2Qrm 4I3A== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=kvl1Wqim; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4001:c0b::22d 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:mime-version:from:date:message-id:subject:to :x-original-sender:x-original-authentication-results:precedence :mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=+FLqqMMBSpJQKZS3r9CdosloQz6czGRgqxHi34Wuhsw=; b=WIb6yxNZ1j4LY63Vx8WgQwxsEaBmOlfai4J1W7OWm54meCUQLRnLybK+LreW9CyViC XFrxotlkPvVX0n+OuWRRhA+7CuNhOfkngYqHZHWqGaaxJOq3zx8t7ux2DNXKTIAFaLSZ 63TazoZSa9+iDGeG9FircAILeIasCr/Qblp8SU4/s90IQbaBDeu8EuzT4iSAV92zQm1N VB+nLRmUQW0WZvK6m13GgJV9aKAzW5lZKjZEZZ+MQbrQkclfAgpI3a2TiWwPGlFJ609g 12z8wqSuzr59XEVBVrEzTcoEJiP0HoUl4JkV0fKelSMxh5rW9jkzIVsYmFpxicNIN42P goIA== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:from:date:message-id:subject:to:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=+FLqqMMBSpJQKZS3r9CdosloQz6czGRgqxHi34Wuhsw=; b=ENMyu1mdcwXa6YeZQlqvBVlKVf4iZgi2KUMDs8LuVIcXBsBQArrgiZiHixYDY5hjW5 y2nSoXZYwSNdP/p6GDUIyUlVBa6qQ9vcR02zZNEnd4wofnDbvTXIdxrSWcR5hID5S/zU xTkhWZGIOPOo3V/b83fvdlX3GVwMZLN5ZIy92a6lds2Vf3Hca9wsZ+WvHDFLgVUjqiZR fFA1HnHKuf9vPaOzFpoU13mJzMz+71HpUPAeBS3QeBxEoSfobjopvjXF+zsVBH5iI4mu MWFBc9EwjBL8QaBMQEqTgrrNpbaOwmLJmOkPqRdpFkElyvG8O78EE0XReu6KCBr7kR4Y H9/Q== 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:from:date:message-id:subject :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=+FLqqMMBSpJQKZS3r9CdosloQz6czGRgqxHi34Wuhsw=; b=VdFMQ1P6MjlDGrbxvv7gikKdjXeKwNRQ5duzX/2+Mzt0kpALVosbvf1A4/j/bW5GDp KQ8rqYfmUWpJTLD4aaIs80E+l4UhLK9pbrvk9QvV6wUFVlFQ7aO5t28okKbyXgC1mvzf VDTWKyzg2zWu9l47emZT392AXrwnLedFP4+Fwiqs+b344PgCdJSFypnA4Ug4NAp6f5/k 2qEHYXtQQsFANEPI7eYMgnSorqq1XY58EAwpjfKyKlca4xTLj1/5mIiyS0Y28NErURnw UiynO+n4WlREu4BVBsMNb2GJQDiptB6ZDVO3m5Vmr1wLzR2sbMd3/UmxHGilENgYfkY1 R5VQ== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AOUpUlFJuMx/BKEOwag0rtv6Yfs1iSqV2gor0qVsLwJ7jzPt+QaFot4t sdP1XhXyY8bn9WLra3ZrorQ= X-Google-Smtp-Source: AAOMgpdu/pbMQzqckjrv/YjcJbcE0rRN3d3oqIyD/ALz7w/07Mclq3geLPsOIupycrVEQ6MkbtchlQ== X-Received: by 2002:a0c:b98d:: with SMTP id v13-v6mr313861qvf.0.1531977517930; Wed, 18 Jul 2018 22:18:37 -0700 (PDT) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a0c:9e0a:: with SMTP id p10-v6ls2793932qve.6.gmail; Wed, 18 Jul 2018 22:18:37 -0700 (PDT) X-Received: by 2002:a0c:e801:: with SMTP id y1-v6mr4695511qvn.55.1531977517729; Wed, 18 Jul 2018 22:18:37 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1531977517; cv=none; d=google.com; s=arc-20160816; b=YI+qHbCBQTdEEtp8+Yl6rkrcMrKU3zaj+6nOdN14k9K/Ke5JBrvdQsGDRJaW/tDGny EmnwDVdTzzpFj38jYKbDAi7zHcKy9ugDkeTNk9B5tB0h9k1A3oLEG7Uz+s3qswVzLi57 e7I2w39hOLA5iaPns+umtWaVJeAFqGZ3cyScJHAf6T3JEJwrKDCMkqgcMcopGlk2QcEU UzAwGn4IpCDQ1V5FbLu1w5ncMIvZf9dSfJ3GTHFtdmMW9Ltmambh3+nXAmTxIONfQpsW m4sQWWJ7kRckRMSvDkQmO5aytnL1h+5cjFb7Xc6ut5KwYhjqzDtMbq358wiXbtymXf7e S5Ng== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:mime-version:dkim-signature :arc-authentication-results; bh=p/g+SN6Acy4exWOlEcMlUXanyTLG5tJbkWYWI8r04Aw=; b=T1Jxy2dmU9MmFc1ZJqfie1b7xmDIaGuncKkolBJStDrL1mqrZ88/DaF3lsKqtQ97VY luD778qgiToM38cXPqjThaQnov1+HPY2gqXstwxD4UOFMByaaKX6udPHpBsCEFuZY15y QlU9SM50fMyTKfWey2XmVxT7mej/z1dSpeiJTpxn8wMRTQBEWq+PlVrTlUH/qvc2ndMC MfoGQbYcQB48srj4hJcARdqbDWWe3NIMR0kcqYc9L6MWxTEeyb6nfKN0BqRkAyu7IsEJ 4N4m7qyczAATA4orDH3E3KhyTrS4xCZwk1030cJKSGDRbAsJOt7mDCu9yU+tt3bgX/xb IpWA== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=kvl1Wqim; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4001:c0b::22d as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it0-x22d.google.com (mail-it0-x22d.google.com. [2607:f8b0:4001:c0b::22d]) by gmr-mx.google.com with ESMTPS id b62-v6si296341qkj.5.2018.07.18.22.18.37 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Wed, 18 Jul 2018 22:18:37 -0700 (PDT) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4001:c0b::22d as permitted sender) client-ip=2607:f8b0:4001:c0b::22d; Received: by mail-it0-x22d.google.com with SMTP id g141-v6so5246248ita.4 for ; Wed, 18 Jul 2018 22:18:37 -0700 (PDT) X-Received: by 2002:a02:93cb:: with SMTP id z69-v6mr8301388jah.125.1531977517107; Wed, 18 Jul 2018 22:18:37 -0700 (PDT) MIME-Version: 1.0 Received: by 2002:a02:6418:0:0:0:0:0 with HTTP; Wed, 18 Jul 2018 22:18:36 -0700 (PDT) From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Thu, 19 Jul 2018 01:18:36 -0400 Message-ID: Subject: [HoTT] What is knot in HOTT? To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000b610fb0571534f1c" 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=kvl1Wqim; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4001:c0b::22d 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: , --000000000000b610fb0571534f1c Content-Type: text/plain; charset="UTF-8" Dear HoTT group, I'm thinking in the following question: What is the type-theoretic definition of a knot in HoTT? Thank you in advance if you have some answers. Sincerely yours, Jose Manuel Rodriguez Caballero -- 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. --000000000000b610fb0571534f1c Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Dear HoTT group,
=C2=A0 I'm thinking in the follow= ing question: What is the type-theoretic definition of a knot in HoTT?

Thank you in advance if you have some answers.

Sincerely yours,
Jose Manuel Rodriguez Caballer= o

--
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.
--000000000000b610fb0571534f1c--