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.1 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-yw1-xc3b.google.com (mail-yw1-xc3b.google.com [IPv6:2607:f8b0:4864:20::c3b]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 6dbfd7b5 for ; Mon, 17 Dec 2018 03:06:28 +0000 (UTC) Received: by mail-yw1-xc3b.google.com with SMTP id d78sf7937939ywa.19 for ; Sun, 16 Dec 2018 19:06:27 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1545015986; cv=pass; d=google.com; s=arc-20160816; b=j7JUvrYDe1d/5XfDTw4s6lxgFhpxCSzBnjanqIeTdQhFW3z1PDX7XvdwRQ2PfzgSRB ujI5/RQzCbtEpq4RgqnbIe+VkwpPsa5oZ0zGLV0KHIbgAhkuA1TFV/y3H5x64GjhfB2l 04Nix+gLgbA/KJm6VODoZY8FO5x4NGDWyyUlrIJyliXDDenClno9iWO3/lf9hBn7366k OGDbWg9GTBMlGCIc5K80V+AelettLftcm+4gWJXnfuT3r1y9r0BQWb3wMrSmCNHlcNaP kWOFkl7X3dFP2FPLqQ+hNW2jkgHuUrm0+afQFGeYoHE8jbCxv65RRcJEpUOprPXPXIPa 9YOw== 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=SjpL1oObnykT8PTPTTe7O3ymuF1U2jSWwiUmzTbPiz4=; b=LqKynzihE4BwMzerjlv6Exy7rbRvqZL3hdbc9/rzBpkqr6KW4G/s+ipVIZl2jzOJJ3 q14Dlv7J+Up9Ar2FQAW+2lW8e7dCCUIZwNAzv7aYCevTlK4vlQcJvhIARYZ3gEWme215 ieJzJ4Iyz/12d9hXcdrkQaiNzYGi0qnTGC1PZuswBxJ9KN/e0ax3pWQytG7AA6irNCOs BNSW+giSXzG0wJ7+tDvkLAx1CbHK0/i89hs9EwoO7zpZR+Nbi3j7h7qZsYXcrKXgmdH5 jdAQnJIkxlMyUROKijafAKe+0z/SfDyF6zrv/DD+Oi5gE7YucdYxRwzcbljIQ5Ucf4NZ rQ6Q== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ZNEdl5ua; 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=SjpL1oObnykT8PTPTTe7O3ymuF1U2jSWwiUmzTbPiz4=; b=CblizufE6CdSOGLuoKYuH0nTIhfzRJtQrdZBb9B8fV5ygB0pXjaiqjwqT6Y/goSB3T MxEFfs4LHIqXMpmHQUnFpt4H/m12CIoYLWZZ601EwtUGJHLx4u5yDEWo3e2pgSf+7fz+ GAj5wUAzzxQn4j3NegEIuH728Oo9Xb72sbMwEmXqlT4rHqwDQ72Vthjbvz25AtNvQ1LJ 76G6EuaYpY2ChxMd/HAcff27c8JM/TJMNS6/HaroyZAYnZ9Iatfrsvw9hY0rtbNiL4CW DA5u8xV3ZX8M22a8eTnGrAdLh1iWH5o+UUfHI+QLhLrkhwEFdfhXkLc4YvmB4t0Yst0e jiNg== 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=SjpL1oObnykT8PTPTTe7O3ymuF1U2jSWwiUmzTbPiz4=; b=Z6zBWPFiVDixpRRWp3Z+Pe6phYybfwC0CouEnLjbGvzT585j3f+QzIVow01sYZ0TLe LuWOUfG4akYk49taAR1pCAML8zA5fWPkHcT1dPxADRLyR15bQogpFmsSSssl3rQwXjWR dlspv8KAhB+/1L/OjJSvJI2DBWcKfTmVqFSX6h/t5lVvI+HqNgzUM/U8aQw+PZgrJa24 JzcY5SNMlaUuOe/rqwga4aecj88vfaQ1TS6LPRPXabBDz6k4xVQ+XICW1vEIbuaxi0LN l8O1QkHDOfj9mKvcuZNsMUIhXfpjjpY8aJTp1S3lLkmICHXQizXatOQRmmh2+VMTS+4o n5sg== 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=SjpL1oObnykT8PTPTTe7O3ymuF1U2jSWwiUmzTbPiz4=; b=Mb193hYhiMD3pBJIL6GTteccC14jGnyV1DEPvlZkAGwCl9Vy6dCjkW+VM6u+iTOmXZ JXna/bBPCXfGVjPkP0FMWkRP9tXdSPdMWRvMO17R2X5UHyl4JuEMdvN7hgYQBrqzW7T5 YsdPyQesnxbL5gz1tLTx/2uyJYmZHzhW6xcYA8egjEBH0vRKopDq9uxDsInnBxOBPtLM SS3bLY+lDE+SDsyVsGRy0uuxqMe/8HuLLtorUHrpKck3RxPNCss8UfXtotCsXIQ3bQ6s in5SyN32qUjGTC7/LBXVKnfDfqer2/IVjO/+0MG8Jrpcrx6jPh2N3owLXNayMi6tjuIs NR4g== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AA+aEWaXURX6z41iHSNhZhk24oLuiuGP6DBDRBgIsBz12+7vYWxtDPjF epJeo8BoUK7LEHjuF2whh9k= X-Google-Smtp-Source: AFSGD/XmZr3409yyFRf9TOR9rt2LJW/2zWN26CEXh3fM8dZsojnVuAuIMo5gG+WZB2lzMRpy2hgQMw== X-Received: by 2002:a81:9841:: with SMTP id p62mr137036ywg.0.1545015986528; Sun, 16 Dec 2018 19:06:26 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a25:b812:: with SMTP id v18-v6ls3186552ybj.14.gmail; Sun, 16 Dec 2018 19:06:26 -0800 (PST) X-Received: by 2002:a25:b85:: with SMTP id 127mr7240895ybl.19.1545015986230; Sun, 16 Dec 2018 19:06:26 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1545015986; cv=none; d=google.com; s=arc-20160816; b=hu2eLvcQbWUCs5eb5SX5vH1lKlTCO83+B0wDgijJtmUKaWde7+vBeF70jttETlraED ZMhSrw1SDGYPVNV06lMuSEoeVFrKSniKkvcjMZsOZwoWGw4ciQ3C7S+I5lNe39uaM4Qn 0tf1ESts+2pS8G/opPswr38u3jhpMqaBm9cuj5Ha0L6M+fFZLkIlG5pvsiPP9OMXXvkc qTenBTxD4BzHgWLXa3oQRPXLoghygLmbgj6apn/3r9gpa3PDYPE6QjLSjzSXQzXxgAku rkHHe7T5rSA0Aac9PVjlISwutVF9x+kMBtG8rBBTat3IzGhVOkF5dW6TKvlIr49yOnM4 iaNw== 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=0DHiUVG/opN297serxPPIo2YAa/fmA86VLRsphSeHkM=; b=Cw0n3RQu82cx/xjJhXBZxTKT1vUFyJReOTzqcGSi/skYBuE69q5Fh5JhixVPMTAZ0d w7/9PaCTANZ8t0kRRSM/ufVj0+Kh4cs1+OCDBTucN2++C94SvSBJWAwIueo+9sqeU4W4 uAP2nsfSU10EBvizM89Rc4DYDhpYg3HkPgFnmm2tsJ4PdXx9vPH4n56eQlwmG9e1VDuH EGMKAV8300fXQP21G1vIfegFxtCWrrln1B7S2+RllOyru7ynTKC1o8CRYlh6IjQ8oG3z uFxaBet5Up5SSLcqpeeo24g9TbS9yS5HbNOgVJF61wnUy8lHzinZpVCVcIn9SQJpmapb +sXw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@gmail.com header.s=20161025 header.b=ZNEdl5ua; 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 l189-v6si524288ybc.2.2018.12.16.19.06.26 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Sun, 16 Dec 2018 19:06:26 -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 b5so17871922iti.2 for ; Sun, 16 Dec 2018 19:06:26 -0800 (PST) X-Received: by 2002:a24:2912:: with SMTP id p18mr10653267itp.16.1545015985663; Sun, 16 Dec 2018 19:06:25 -0800 (PST) MIME-Version: 1.0 References: <20181214071146.GA19128@pachax.iitpkd.ac.in> In-Reply-To: <20181214071146.GA19128@pachax.iitpkd.ac.in> From: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Date: Sun, 16 Dec 2018 22:06:14 -0500 Message-ID: Subject: Re: [HoTT] Quantum Computations and HoTT To: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000ff7835057d2f1003" 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=ZNEdl5ua; 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: , --000000000000ff7835057d2f1003 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Thank you ppk for the reference. My main suspicion that HoTT may be useful in Quantum Computing is the idea of the topological quantum computer, although, it is just a suspicion, not a claim: https://en.wikipedia.org/wiki/Topological_quantum_computer Kind Regards, Jos=C3=A9 M. El vie., 14 dic. 2018 a las 2:11, Piyush P Kurur () escribi=C3=B3: > On Thu, Dec 13, 2018 at 11:06:37PM -0500, Jos=C3=A9 Manuel Rodriguez Caba= llero > wrote: > > Hello, > > I am interested in the formal verification of theorems related to > Quantum > > Computations. I have two possibilities in order to do my formalizations= : > > either I can use simple type theory (Isabelle/HOL) or I can use UniMath > > (Coq). Does the homotopy type theory has some advantage over the simple > > type theory in this field? > > > What probably would be interesting is the linear variant of the type > theory (whether it is Hott or the standard type theory a la Coq). > > https://arxiv.org/pdf/1210.0613.pdf > > I have not really followed this line of research and hence have > nothing intelligent to contribute but if you find something > interesting or you already have some project going on, please do let > me know. > > Regards, > > ppk > > > > > Kind Regards, > > Jos=C3=A9 M. > > > > -- > > 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. --000000000000ff7835057d2f1003 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Thank you ppk for the re= ference. My main suspicion=C2=A0that HoTT may be useful in Quantum Computin= g is the idea of the topological quantum computer, although, it is just a s= uspicion, not a claim:

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


El vie., 14 dic. 2018 a las 2:11, Pi= yush P Kurur (<ppk@iitpkd.ac.in&= gt;) escribi=C3=B3:
On Thu, Dec 13, 2018 at 11:06:37PM -0500, Jos=C3=A9 Manuel Rodriguez Ca= ballero wrote:
> Hello,
>=C2=A0 =C2=A0I am interested in the formal verification of theorems rel= ated to Quantum
> Computations. I have two possibilities in order to do my formalization= s:
> either I can use simple type theory (Isabelle/HOL) or I can use UniMat= h
> (Coq). Does the homotopy type theory has some advantage over the simpl= e
> type theory in this field?


What probably would be interesting is the linear variant of the type
theory (whether it is Hott or the standard type theory a la Coq).

https://arxiv.org/pdf/1210.0613.pdf

I have not really followed this line of research and hence have
nothing intelligent to contribute but if you find something
interesting or you already have some project going on, please do let
me know.

Regards,

ppk

>
> Kind Regards,
> Jos=C3=A9 M.
>
> --
> You received this message because you are subscribed to the Google Gro= ups "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.

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