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=DKIMWL_WL_MED,DKIM_SIGNED, DKIM_VALID,DKIM_VALID_EF,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-qk1-x73a.google.com (mail-qk1-x73a.google.com [IPv6:2607:f8b0:4864:20::73a]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 12eefcbc for ; Mon, 7 Jan 2019 17:58:24 +0000 (UTC) Received: by mail-qk1-x73a.google.com with SMTP id y83sf912313qka.7 for ; Mon, 07 Jan 2019 09:58:23 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1546883901; cv=pass; d=google.com; s=arc-20160816; b=M+s9GYYT/Z2KjagBvqhu6Vx49GzHLIvqXb9JeK99HsEIW54jk9nkULKYemsEP2GJ1T pOjbfeLSdUv3P3pZNbNsyVW2Hx1Npg3/m9023TUCJb71iC5mHUzTMDoci4MkXfd56Q2/ /Pv8Q79npBKcbuubWjadqptzh4htwV/xoBJieaWC4JxjrkeYMMdf5VzJf7o/6UxOwCLf jKiJpuLmTCtihfbnYaENrqDJV9rTCOhPOuBzsW5cPsu5lSvjAWzkwyx8xXpAs1M3Pe0J ROKqgmfAUB9M2piV+YQFSgbDzvhpEP8DAoS3C5Ta2RMaHP36Tq/wDXgKwXavDJDY9MS3 gAZQ== 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 :in-reply-to:references:mime-version:sender:dkim-signature; bh=LvZ5DUMeb8vmPD8x+Src/8399df7A8n6hUVsjOQ7pI4=; b=S8khqUa2cwpxhN8WjapeY+MleHozVWg6H3QuNG+c/7VfSK+UoZNXgK8tZu7+X8cjsw GifWnV+f9nRgFxQ2h1vK7/JNRdRQLHjpiyV6d1oRLa+gEzOLB9I5c5o5TCJch9cVxIh/ 2ftqHkvvQl15Ft9xgoa3SgqwX7ewJRN43pNDigSlBH5gaZMjxj8mj7iLliyUx1OoDy++ A7CBjqqr0FbVn/6sZ0oRv/1OtBuaydG3Hsm0mDUoZmWmrCvAJdQhPEBu1Vkv1zNSWtmX rK5mx1Y/7YcZR2hjXQLQl1qUnrbBJF54+0i/PxvBTHb5rRDHh3AODZWUbct/RRf+6BfB gQmw== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@galois-com.20150623.gappssmtp.com header.s=20150623 header.b=kFOlPeQ3; spf=pass (google.com: domain of langston@galois.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=langston@galois.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:cc:x-original-sender:x-original-authentication-results :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-unsubscribe; bh=LvZ5DUMeb8vmPD8x+Src/8399df7A8n6hUVsjOQ7pI4=; b=GVRKdI4TT/9HSgTiz0Lb8GbLyNLfeQKmrMUyE6283n4qiE4u7MbsWNGT5fVCHFu7PF 5BA8tZu57k97/HDj8MhAO1zRFAJo6r8IczGqxDl0FiIABNmLSnsut+IyZpWdWzhdM9gH X+0999IJH+hIoxsubHwzb8/NQ/7mr41nJotuy3KKDs53HdGZFu2cM7IShtkzsOHBnIzr PihSyQzJetSjJbx3u/rZqlhKnNG/OjoryGvAKdcFVTFJmydy1F/L4yGUbJbX6htrLcWf 547CCWh50irZrYtSdUTXTVTlPshd0oJcFXMZhO0IlVfQlcwAE2VUCV6K1Yc4qsL1IQ/o hv0w== 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: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=LvZ5DUMeb8vmPD8x+Src/8399df7A8n6hUVsjOQ7pI4=; b=lOxRe0P7SlTjJH1uNdeycjjb/Dn8GgBH1xhyFF5GrIj3JiYSvVhPEyOwZu72gxhD31 jEsCY/hsbGBEEa1twu2TA0v5HJvxvAinNPt4CpqU9hltd842zN3qqVIAizQXpS5qWno4 thTXyDO07G/V8yRacu+nx2GEzWzpjWF9FQuKOokVWRwg5Khr8MjSML+uXnCjhN4Iy+ng 7qmgoyCkoGNbwi2vKais9MqoVnNQS1q1R/Yt2vjINdzfUFz3IiRsYhJR+0n+qPScKUqK dBBQ8UXTpRfwEvRt7ba4M0ge59Y3TM2Rk5z0fJOZCBCtWitb6hYTYeSjD6pZQaPETqsT OR4w== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukdLd997kWbtUh0/490KxwNS+4CBJllZapUGCFbsIDO7aBY7Ipzc vGm+zyv51kT0UergstRueGw= X-Google-Smtp-Source: ALg8bN74K1tqelQZyYer7anbqNIMKspXYB+AOFarfH3VwAUavNYoR5bpXN9SgWNzTba0I48zpzeVqw== X-Received: by 2002:a0c:8b4c:: with SMTP id d12mr1009621qvc.3.1546883901540; Mon, 07 Jan 2019 09:58:21 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a37:7f86:: with SMTP id a128ls563938qkd.6.gmail; Mon, 07 Jan 2019 09:58:21 -0800 (PST) X-Received: by 2002:a37:4e8a:: with SMTP id c132mr46357455qkb.13.1546883901111; Mon, 07 Jan 2019 09:58:21 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1546883901; cv=none; d=google.com; s=arc-20160816; b=cMoxvA3N9u6WBg/vrV14NgJOWf7VnG7IJ0KxkJTbLYiKYRUms5CoXKyD9tshCTRZNg hsEf9/1/CE1b60pQCvoSZAAFfiIZYZGnzOLnIwvyySg032/5Q+EMKPSI90j0iSu0xWQb 4xFRkdw0n5vOdh7Nz/TSI58Vve9XIDgimwBkybWOYbKM6+5ShByKxkfOC1ZaHJs//+b3 PP6WRkKq0LN6LzBettZzSxiWT2Ton1hCqPY3z7rFvhOVSDUbYyuPhYuYjgOCQ2GAD+pY 1GlmH20TgG2PCB1UoWqWHfT1XFr4P+VCBJhG7arL7sCIY/yVI7WAdhExbQCloD+rwRpH ZiLg== 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:in-reply-to:references :mime-version:dkim-signature; bh=2RlalC+azs4+dAwQoIeiBVY3wYIH98Ghsm5bSb9sXUA=; b=SRzVLWsjqA/Gkp4fd36hT9nJkR0P1x57yKlMpRRJKf+qMQSOwvrTc6JtjzHcLUbqVR KOOLz2xJi0z4tSdXi+tP29pQfUbulhi/b/9CAsoqDGZztQ3FN0D3lJKC6K7XGw1HUk01 7MRVY39e8OF5U/zKUHA80ii8S9ee608FudnCctSXmr1TV0SiJ3i43mXXJ96TMvn+D8Ac FQy1tt8h8IPyGfpXKkKRtoTKCrUOVtx55pLk2epmPe5GnC56Y6y/1MVTJThpNwxvLM/9 RnP4SRfj0fvwng+kNEta6Zepl3ovDCox+vufv4W/cpAGZzC+2mISMQh62wEPStO1eafS o5Hw== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@galois-com.20150623.gappssmtp.com header.s=20150623 header.b=kFOlPeQ3; spf=pass (google.com: domain of langston@galois.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=langston@galois.com Received: from mail-it1-x129.google.com (mail-it1-x129.google.com. [2607:f8b0:4864:20::129]) by gmr-mx.google.com with ESMTPS id b25si2704189qtq.2.2019.01.07.09.58.21 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 07 Jan 2019 09:58:21 -0800 (PST) Received-SPF: pass (google.com: domain of langston@galois.com designates 2607:f8b0:4864:20::129 as permitted sender) client-ip=2607:f8b0:4864:20::129; Received: by mail-it1-x129.google.com with SMTP id c9so2292668itj.1 for ; Mon, 07 Jan 2019 09:58:21 -0800 (PST) X-Received: by 2002:a24:d203:: with SMTP id z3mr6743832itf.156.1546883900704; Mon, 07 Jan 2019 09:58:20 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Langston Barrett Date: Mon, 7 Jan 2019 09:58:09 -0800 Message-ID: Subject: Re: [HoTT] The best proof assistant for HoTT from the point of view of automation To: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= Cc: HomotopyTypeTheory@googlegroups.com Content-Type: multipart/alternative; boundary="000000000000691de4057ee1f945" X-Original-Sender: langston@galois.com X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@galois-com.20150623.gappssmtp.com header.s=20150623 header.b=kFOlPeQ3; spf=pass (google.com: domain of langston@galois.com designates 2607:f8b0:4864:20::129 as permitted sender) smtp.mailfrom=langston@galois.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: , --000000000000691de4057ee1f945 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable While UniMath doesn't use much automation internally, Coq has very rich facilities for it. Using UniMath as a base for your development doesn't prevent you from using e.g. Ltac for automating proof scripts. Even if you decide to develop without using Coq's automation, I would bet you'll save more time by reusing UniMath's extensive development of category theory than you would by using any sort of proof automation. Here are some resources on automation in Coq: - Tutorial: http://adam.chlipala.net/cpdt/html/Match.html - Reference: https://coq.inria.fr/refman/proof-engine/ltac.html On Sun, Jan 6, 2019 at 8:57 AM Jos=C3=A9 Manuel Rodriguez Caballero < josephcmac@gmail.com> wrote: > Hello, > After reading the (beautiful) paper > > Paredes, Bel=C3=A9n. "Boson-Lattice Construction for Anyon Models." arXiv > preprint arXiv:1804.01605 (2018). > https://arxiv.org/pdf/1804.01605.pdf > > I was rather motivated to explore modular tensor categories: > https://ncatlab.org/nlab/show/modular+tensor+category > > using a proof assistant. My preferred proof assistant is Isabelle/HOL, > because of the hight level of automation, but I am not sure that simple > type theory is the best formal system to work with modular tensor > categories. As far as I know, HoTT has been used in order to formalize > category theory in a rather successful way. In my case, I programmed a > little bit in UniMath (Coq), but thee automation was almost zero (maybe > there is some automation, but I did not know how to use it, everything th= at > I learned in computer sciences was self-taught). > > So, I wonder in which proof assistant HoTT can be used with a maximum of > automation. > > 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. --000000000000691de4057ee1f945 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
While UniMath doesn= 't use much automation internally, Coq has very rich facilities for it.= =C2=A0Using UniMath as a base for your development doesn't prevent you = from using e.g. Ltac for automating proof scripts.

Even if you decide to develop without using Coq's automation, I w= ould bet you'll save more time by reusing UniMath's extensive devel= opment of category theory than you would by using any sort of proof automat= ion.

Here are some resources on automation in= Coq:
=C2=A0- Reference: https://coq.inria.fr/refman/proof-engine/ltac.html

On Sun, Jan= 6, 2019 at 8:57 AM Jos=C3=A9 Manuel Rodriguez Caballero <josephcmac@gmail.com> wr= ote:
Hello,
=C2=A0 After reading the= (beautiful) paper=C2=A0

Paredes, Bel=C3=A9n.= "Boson-Lattice Construction for Anyon Models." arXiv preprint ar= Xiv:1804.01605 (2018).

I was rather motivated to explore modular tensor cate= gories:=C2=A0

using a proof assistant= . My preferred proof assistant is Isabelle/HOL, because of the hight level = of automation, but I am not sure that simple type theory is the best formal= system to work with modular tensor categories. As far as I know, HoTT has = been used in order to formalize category theory in a rather successful way.= In my case, I programmed a little bit in UniMath (Coq), but thee automatio= n was almost zero (maybe there is some automation, but I did not know how t= o use it, everything that I learned in computer sciences was self-taught).<= /div>

So, I wonder in which proof assistant HoTT can be = used with a maximum of automation.

Kind 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 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.
--000000000000691de4057ee1f945--