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, MAILING_LIST_MULTI,RCVD_IN_DNSWL_NONE autolearn=ham autolearn_force=no version=3.4.2 Received: from mail-qk1-x73d.google.com (mail-qk1-x73d.google.com [IPv6:2607:f8b0:4864:20::73d]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id 8aaa7dfa for ; Mon, 7 Jan 2019 20:57:26 +0000 (UTC) Received: by mail-qk1-x73d.google.com with SMTP id s70sf1382268qks.4 for ; Mon, 07 Jan 2019 12:57:26 -0800 (PST) ARC-Seal: i=2; a=rsa-sha256; t=1546894645; cv=pass; d=google.com; s=arc-20160816; b=r4UdC7upj7/9vlv9YMl7xOSEXEzZWMxKN3Dh1lnq4vrwN4PEy6CPZhvX5KGNpkstbG 4z3cgs7k8PZK1KCgusqlLo5SkyjsIB/fVWvumy3tIj/KgogEnREroncJOv5TTXgIHiC1 jtM7UUrvw8/eys7J48qcxR5FPCiLPSy2C92S4HvEtEiuVvy4Juo8jHzDdjarxnBytkvw hN2naRa/hO6FKypgQhhAOqv2Geoh/5fo8FH0EQF4M6zzCXViC0MWY6RiBpCJY7y5n1HZ lgwYJZERztNlhVKZz2CUpsC2zjphyypgPHXTBGI1TUaPpdF2pBgfiIiOkVtd5zfdkwtx An7w== 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:content-transfer-encoding:cc:to:subject :message-id:date:from:in-reply-to:references:mime-version:sender :dkim-signature; bh=QfwHHJ7r4X8BhBbd+KvTervmFoKpjGqmiRXRvd5lKr0=; b=HODFSKA6LMFCuUTfcCK0ejai4sYlqpkOGIlxs7SwH7GFx33mxqljLsk3CLVeT1fkDl Hwa+Bm57+uuuWNaTQEzrv1dQcn6zWuksLcitdF1oueRXaQhZ1/yHKVqDcy3ufg74tgDp IT3fRvs63fJCq7ZnGJ5AKY7beyiuHlwPz5HvopI13vsudMvbeQr9qvbzIWw89jIqiZ25 EfMGJVEQ8ULMLwGweusczTkWCTi6sf3DwlB5wa5PBQLw8soRAhR00NF3no6rQ4e/gOAL yWGvWTCPDcNG4atw+YjeexfafTwPMytI9oeBZwbf3dlnceQbtFwAjg3WFBSlLLlnPrDX Tp2w== ARC-Authentication-Results: i=2; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=0witye9L; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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:content-transfer-encoding:x-original-sender :x-original-authentication-results:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=QfwHHJ7r4X8BhBbd+KvTervmFoKpjGqmiRXRvd5lKr0=; b=IzERvHy5QSEXFv51TyWcrK9BuoK2ul5yOo1e+XDJOytHs78+tRnlzckV2FGcWu2feM TdoXxaK3bkonSXhmYj//YOD2xxCFT/niOHGN/kPOzlDcKi0lDAefL/CuJnXsG6pHaJZu 3iGlDI3vHzR8U4HAb4wHqQzElbuWRbXUItiwrY8JiaMSFNBxOx3PqA8Ou8P5+g+lihK2 Z7mGv5FLmbsACXrh6HiBjc+RFQtqImmeemubNhY2qc+OguJCJu9fFKSsIEiGgQzF9n3v o3JyUyrsXMgkAwWDEVH1zjXz6/+SmiXQd9Xj43kCmvbzmF/skGvLMlAUCANcooGfKs+7 ZCCA== 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:content-transfer-encoding :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=QfwHHJ7r4X8BhBbd+KvTervmFoKpjGqmiRXRvd5lKr0=; b=Fox7mQBw2vH7ZaDl0yJIfpSS6TxI2FoMCkGYSjDfkfFcibWkeZ4ug7O1ltWowCRRDl zYojgeXQBmgyBf3Wq2tuNkHHW1M9//0q9aigTEY6nQErQcVHvmYHF95qIP3vIWkoiFBl tey1rIs9Ccb3ZWkXP94j/VyMNpAnPH+wNhZMkBoehskrFXkercaedSC9dqgeiyeiIQwL AsyOGmZzA8WKxdJnx/G6c03aoW+IRVFkZsjKlAH051Xe6cO+eRgVXlKvPl9EChu9QsKp Qsw0vAipigKyUkSon3+bWm83vcBozAp2HwCuBiHn8nRoUEqGxk4ZyUCANFGNHLCUOk5M TkwA== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukfs3+zqUND1giv/+7F7wsWNcproA9hmjVQnHqvdjMsEQenRWdmg OdBmvDh9XfpVChE2UC4azjY= X-Google-Smtp-Source: ALg8bN7z/yaNZd1lHnNMsz+fThtP3KAMdYsg95u1riqTQr3bz+Rjt36h15OUjM2fin0V/relmsH0oA== X-Received: by 2002:a0c:8b4c:: with SMTP id d12mr1016780qvc.3.1546894645836; Mon, 07 Jan 2019 12:57:25 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:ac8:2201:: with SMTP id o1ls869914qto.2.gmail; Mon, 07 Jan 2019 12:57:25 -0800 (PST) X-Received: by 2002:aed:22cb:: with SMTP id q11mr47442248qtc.31.1546894645545; Mon, 07 Jan 2019 12:57:25 -0800 (PST) ARC-Seal: i=1; a=rsa-sha256; t=1546894645; cv=none; d=google.com; s=arc-20160816; b=QegOwwZnyP4+nNFScKfKnEhitRwz+Rp8dip4zDQ7CvZ3Y7hbPI+MD9+P/FR44jBa7a 4zbwpDWOOsShLzmu9cxn+suzFtxDSCHbmkNJOW5RvyZSKnl+RZjP6oBoCsjPiOm1ykzf VI1OZ/9TrKujo7QqOFiYjT+63SJEOvoh+h06vgCoyKYRz9qZnyagr5s16Lf4UdbqBE8V nhxL5iCGH6OV7U0AElGHS4kPRWKdJJqlk7xk576nAXAs9RGJDRSoHlGBnh2OBZaKTcds mbMI5zUvBZ++Nzx2doI1PWuj/x2a+s5QgGbSm97BnHrNuFsNjfMQL8JPibmmZYOIWeYI q3qg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=content-transfer-encoding:cc:to:subject:message-id:date:from :in-reply-to:references:mime-version:dkim-signature; bh=SXNWZv55/Etggppvs6ouFPmBnIoBKLkNgT+btqU1juM=; b=l8/jUnn8zeFYnMF5rXyzj676KygfXMJuc5y/jFm7zOfXe8ySFUBqJSxhBwjhlC7KlH 1sZ3xzy1qZgfOsTBOFEzj5w2MMZij3kwn3ygIOfjdyzQEFYVWF7cH8dOuKEIu1cElXTk c3CDHvmt1HYLdfomwiJIx18deKnruGecvR7Z1qnoyr4nX0vNbp8ureLi1qtm57UjahRl 5aQ3rt7S664cGSa0iQy0VSPabOA1m9lxtjHmDJqIAaEoUOasMDz4ufNE0grkFNJ4FDnL oBt5AKb8Z1LVfwUfEIRFSxl6uF6pJfZGNTviFk7kX0gJxiMihNnEugRRsLlhNwXDiy12 Ne+w== ARC-Authentication-Results: i=1; gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=0witye9L; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu Received: from mail-yb1-xb36.google.com (mail-yb1-xb36.google.com. [2607:f8b0:4864:20::b36]) by gmr-mx.google.com with ESMTPS id z129si190562qka.2.2019.01.07.12.57.25 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 07 Jan 2019 12:57:25 -0800 (PST) Received-SPF: pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) client-ip=2607:f8b0:4864:20::b36; Received: by mail-yb1-xb36.google.com with SMTP id e1so709044ybn.11 for ; Mon, 07 Jan 2019 12:57:25 -0800 (PST) X-Received: by 2002:a5b:643:: with SMTP id o3mr45006713ybq.181.1546894644939; Mon, 07 Jan 2019 12:57:24 -0800 (PST) Received: from mail-yb1-f175.google.com (mail-yb1-f175.google.com. [209.85.219.175]) by smtp.gmail.com with ESMTPSA id o14sm34757923ywo.52.2019.01.07.12.57.23 for (version=TLS1_2 cipher=ECDHE-RSA-AES128-GCM-SHA256 bits=128/128); Mon, 07 Jan 2019 12:57:24 -0800 (PST) Received: by mail-yb1-f175.google.com with SMTP id n16so702921ybg.13 for ; Mon, 07 Jan 2019 12:57:23 -0800 (PST) X-Received: by 2002:a25:384:: with SMTP id 126mr55897949ybd.357.1546894643541; Mon, 07 Jan 2019 12:57:23 -0800 (PST) MIME-Version: 1.0 References: In-Reply-To: From: Michael Shulman Date: Mon, 7 Jan 2019 12:57:11 -0800 X-Gmail-Original-Message-ID: Message-ID: Subject: Re: [HoTT] The best proof assistant for HoTT from the point of view of automation To: Langston Barrett Cc: =?UTF-8?Q?Jos=C3=A9_Manuel_Rodriguez_Caballero?= , "HomotopyTypeTheory@googlegroups.com" Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable X-Original-Sender: shulman@sandiego.edu X-Original-Authentication-Results: gmr-mx.google.com; dkim=pass header.i=@sandiego-edu.20150623.gappssmtp.com header.s=20150623 header.b=0witye9L; spf=pass (google.com: domain of shulman@sandiego.edu designates 2607:f8b0:4864:20::b36 as permitted sender) smtp.mailfrom=shulman@sandiego.edu 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: , The HoTT Coq library (https://github.com/HoTT/HoTT) uses somewhat more automation than UniMath, I believe. In particular, the category theory library that it contains (https://arxiv.org/abs/1401.7694) was developed using many of Chlipala's automation techniques. On Mon, Jan 7, 2019 at 9:58 AM Langston Barrett wrote= : > > While UniMath doesn't use much automation internally, Coq has very rich f= acilities for it. Using UniMath as a base for your development doesn't prev= ent 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 catego= ry 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 wrote: >> >> Hello, >> After reading the (beautiful) paper >> >> Paredes, Bel=C3=A9n. "Boson-Lattice Construction for Anyon Models." arXi= v 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, b= ecause 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. A= s far as I know, HoTT has been used in order to formalize category theory i= n 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 that I learned in computer s= ciences 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 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. > > -- > 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.