From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.4.2 (2018-09-13) on inbox.vuxu.org X-Spam-Level: X-Spam-Status: No, score=-1.0 required=5.0 tests=DKIM_SIGNED,DKIM_VALID, DKIM_VALID_AU,DKIM_VALID_EF,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.2 Received: from mail-io1-xd38.google.com (mail-io1-xd38.google.com [IPv6:2607:f8b0:4864:20::d38]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 29899bbd for ; Sun, 18 Nov 2018 13:52:02 +0000 (UTC) Received: by mail-io1-xd38.google.com with SMTP id e144-v6sf28615670iof.13 for ; Sun, 18 Nov 2018 05:52:02 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1542549120; cv=pass; d=google.com; s=arc-20160816; b=hRSQGi2hL529E7guIQ587Ck3mwVx5mL3jJ97VWIRJctW6V4CAXgkMDOIY7wSVFVGzW rL8K9+qZmrDzo1IbM5bwEuXL9M6dfK5ctyAEpzcktJRSa8lbqdvtuZunYLTSMrcAli2h Wat3SLDeK3xanVUJ/D15cp0VVJGccHpJEpEpCvNGz9UCkTl6OJnM4wGn8ZjxOi+SdPT+ VGy1b5CAglPYcePOVDPG+WaPSIODi5INwiuf8dgfBf8yc0nF2ETaxA/4OUulSZz3Xw0t +BvEPxUnKNNhIhrkYdmKOevggiDDwP0ifLW9yzYypRbBU9wuSlw6Un8zQeKq2HUvboCi Jriw== 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:in-reply-to :references:mime-version:sender:dkim-signature:dkim-signature; bh=y0kaGGi2CbH4QD9IJTAv7G9gYU7S37tYU+5BbxqDXrA=; b=dIaOinR8loqx3e323dLIiXZgjSyZzmIydZAu6ZNlrIAX2aQNsNIUMwk8QuaYjHuudn hjUoBa5SC6KaORdfDiAkOK2vfyBrRyCicVCgnO5/x2XRHkHAbVb9f7rCdg4JQ3mQVnT+ KL/EMpuLErMdIvw06xa7SZn+A0tXS0Lyou9Rscgg8ENm50TT8oFTUbhm4ifWg7Y8Nmbd sPZFOZ+S0riBTkk6Y4lVUqOs8OVCgpWmiuCaJzimS13RrBgYg36RIqKxnXulqE5pYXZa 8v7RKvGNjW+kzDcSOS6xS++nKgZFg+JmxV7d7UgwczWHCCcnaYxldeVQgyTsdrfJ/Jm1 hhTw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WulivvqP; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12c 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:references:in-reply-to: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=y0kaGGi2CbH4QD9IJTAv7G9gYU7S37tYU+5BbxqDXrA=; b=mqUk8BJ1ReUKb32ROgCIlK/tcSnVYnjaKFbXQpTu+E/t2FEx3ma6lxC0HKDxKNSdsQ 2tQv0116VP607cs9bjEWn1Of/tW6k3qEzU2Movj1LAJUrIQwzDMsKIxZK6sywDHoSkWf 6ATflPsJxfB1tDzUVMCgumUWRMuJAI/cvVGXoxUPVF4OqMqk9wRx3hHScuV0gkbmWIBo 5MokWGyzkzhjyfiELKxfBs1VliYVXJDXDIMFVsZJVYsh4BjmZgIyYqLsUdDrNu0cukX4 nQM+Kzf+NT4jineA3eZBYE2NiQnGdRmfPQs1I1UcpeOMAr7lxZEWyd7EZrwOmmP31e5f 2mMw== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to: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=y0kaGGi2CbH4QD9IJTAv7G9gYU7S37tYU+5BbxqDXrA=; b=EvJHy+c4ELlnwBXG1As8N9tdnQt7Xcniwiq6bLYxBdW/0VWcJsIZVfn9sR3+gX2kG3 JpkogADPyHq//19FYGgL+yrJWLKRjQNdLkNPaSn12A80pl1+CdqlDINdVtH2uaIWOI9n XKSexNpcpuNUtBmT/F06q/YfuMRFGhG27oDQ49E1hQlJ+E3r5zvx3XozE6pV+Bfg3eeM qD0kYiOHpnfEnH5KWis0pevSNpZfUFsO2RBwcBRyPoeFM7JiUTbmlV6ylQ2jayz4J9si E4FsxiaR0LJf5R5BC7nwGSa6kEpNTvLxiunDFjNklX8ch0K4d+9n6GDj9n1LEXriQAqx covg== 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:references:in-reply-to: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=y0kaGGi2CbH4QD9IJTAv7G9gYU7S37tYU+5BbxqDXrA=; b=bWBcI8Mm839p3qzlZZtOFeEqL4nwJr0qyUQgUVn+PgXPvy0HeoCtoTMor7rht/4cD0 5QM6TUM6zuf+HFR7yKpWedv5+4jjrp5cv1OFQkMhzkgNqhrDHp0+0XzmKuGs/xzJV/9x wtnp6q0+z6hLxmzkbIIVENzJErHq858WOYwZrEWB4J+3XDJvDOlWKOrJOUIAjmqoTWG6 SlvtH42EDbQudiZBUFrHnbLme/Gu4qtB97zfbN50q3qRK1Ho8SaANeNa0jzwfPbdMqqy bsBGgvEJCuPBS9cgyktRxqNZ5HH104sM+mu6T2EZsKVOV+S35AczaWsiBeVB2VWO0qZp QJFA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AGRZ1gIVz0J3IR87b65moewEdvLdkDG5RRC9ZVMNYF9Og9dPPdPfhWWb ZZeuVPzvPBIS0nGY0bTMkDk= X-Google-Smtp-Source: AJdET5cfjxv92iOB6+7kcXhZWRfz3TieVMeBJZsFHmEaw4HAYSVXdeozi57m+n+QvrtXCHlVbWL1Sw== X-Received: by 2002:a02:1e87:: with SMTP id 7mr81016jat.0.1542549120455; Sun, 18 Nov 2018 05:52:00 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a6b:6207:: with SMTP id f7-v6ls997603iog.3.gmail; Sun, 18 Nov 2018 05:52:00 -0800 (PST) X-Received: by 2002:a6b:b5cb:: with SMTP id e194-v6mr9407539iof.31.1542549120174; Sun, 18 Nov 2018 05:52:00 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1542549120; cv=none; d=google.com; s=arc-20160816; b=YC44uE7i20UrX+RhXCq6t7U0sPBWqg07mFCQ5EoYKPjHUGyhtV5i6rcfyofk/bWQeE jIgfgepouhqvZd0aqgxmgcbdaPLbia6KegAyt9afuSj5ac1SaJLCr4kGGU4SC1oyxv+d wG44pBXomXi3sLMr/MD0HcIeduwbt+zGGYjP3Q+wrMMDiWJ0qRPF+4t6yeV0q9ZPbSDk RMSkB9XFHLrwP4UjLxtxH498jWRCgLUpKrb/GKBK/XNwDUtpqAJWWoqMOi6fanlIFc30 Q/kK8+lUx7Y+yOxYI1487kOWGUUD1EjXrT485P+AZtHlAM75eEsHg3sar57khLAylvJg WFpg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=to:subject:message-id:date:from:in-reply-to:references:mime-version :dkim-signature; bh=s/DQXwaadVcNq1jjtX16n3ZlNr2djn4aSbK/nvR0Hsw=; b=E7opANaxf/VRKgp2K9/OCA7RrPSEX8NTN9j6rfBAwgTAJnfAK/J5o71ZucgxO7ndI7 b3KdcROFzaZwEpaN7DJ6Aqia2zCa6E1/WhE7M8XrVk84AAaDQbioPoTUw7b5fHsmKsbp iUjpZ5aKVktq6dbEQaY4cf6RTxjvJCdEjQ6p8NegmZ3qgDaMPlm7THap4+9ZV2AT7RX5 vcZEPwKhB9CdYATcuryWP3LuLs9/aWKZ8INOZ8lgp+gAC6yq2if9BUctE0lERKLh0pfz 1VYxJzXUwAgANfTBMmcZpw35gZT7drTbNsVEWGrxDkk+4UXwK75yF98uoNUis/JZHVs/ gW1A== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=WulivvqP; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12c as permitted sender) smtp.mailfrom=josephcmac@gmail.com; dmarc=pass (p=NONE sp=QUARANTINE dis=NONE) header.from=gmail.com Received: from mail-it1-x12c.google.com (mail-it1-x12c.google.com. [2607:f8b0:4864:20::12c]) by gmr-mx.google.com with ESMTPS id q80-v6si1487746itb.1.2018.11.18.05.52.00 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 18 Nov 2018 05:52:00 -0800 (PST) Received-SPF: pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12c as permitted sender) client-ip=2607:f8b0:4864:20::12c; Received: by mail-it1-x12c.google.com with SMTP id c9so3960753itj.1 for ; Sun, 18 Nov 2018 05:52:00 -0800 (PST) X-Received: by 2002:a24:6102:: with SMTP id s2-v6mr4986625itc.16.1542549119740; Sun, 18 Nov 2018 05:51:59 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Sun, 18 Nov 2018 08:51:49 -0500 Message-ID: Subject: [HoTT] Hopf fibrations and computer science To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="00000000000054b12a057af0b435" 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=WulivvqP; spf=pass (google.com: domain of josephcmac@gmail.com designates 2607:f8b0:4864:20::12c 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: , --00000000000054b12a057af0b435 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hello, During the min 8 of the following video https://www.youtube.com/watch?v=3D3-E1SdSMipE the mathematician Prof. Eric Weinstein (Harvard) claimed that the Hopf fibrations is the most important object in the universe. According to the principle types (in the sense of type theory) =3D homotopy types (in the sense of topology) the Hopf fibrations are a type in the sense of type theory. My question is: What does this type means from the point of view of computer science? Are there some possible concrete applications of Hopf fibrations to proof assistants and programming languages via HoTT? Kind Regards, Jos=C3=A9 M. --=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. --00000000000054b12a057af0b435 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
He= llo,
=C2=A0 During the min 8 of the following video

=
the mathematician Prof. Eric Weinstein (Harvard) claimed that the=C2= =A0Hopf fibrations is the most important object in the universe. According = to the principle=C2=A0

types (in the sense of type= theory) =3D homotopy types (in the sense of topology)

=
the Hopf fibrations are a type in the sense of type theory. My questio= n is: What does this type means from the point of view of computer science?= Are there some possible concrete applications of Hopf fibrations to proof = assistants and programming languages via HoTT?

Kin= d Regards,
Jos=C3=A9 M.

--
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.
--00000000000054b12a057af0b435--