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.2 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-oi1-x237.google.com (mail-oi1-x237.google.com [IPv6:2607:f8b0:4864:20::237]) by inbox.vuxu.org (OpenSMTPD) with ESMTP id df7f8019 for ; Tue, 8 Jan 2019 01:06:53 +0000 (UTC) Received: by mail-oi1-x237.google.com with SMTP id j85sf996277oih.3 for ; Mon, 07 Jan 2019 17:06:52 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=googlegroups.com; s=20161025; h=sender:date:from:to:message-id:in-reply-to:references:subject :mime-version:x-original-sender:precedence:mailing-list:list-id :list-post:list-help:list-archive:list-unsubscribe; bh=2VL3Jdu1Dns+XgkOkVt5HLwV5uieYI5WFoEiXKyvXZ8=; b=NKwmNvwv3kf7UG0bxYKlsjlv/YMrSCnkJgvJg/ThLGeYi3e8BPvS776LPlvLnM6fEx lnw+JJfkLX17hG1b1nT92lUoGryjtgvHq0hO3v2knOS93dC7INLKwoilazSPrAO08VtK 3oBrci+opMRLJF5AE3VCcw3EsLUFLHAutRsbIScvvmz8FPAk41tDmFWKMrLQR5VNYSda hXiO2pu80xzF2pxDtuH1SO4Z6VzAIFZLbd4Ejd8RTOyJS9k+d2UM01l4TggMIQ2u+iv2 3HLcDh1aC5GPo7Crr8MyfO0eo09Ofz7ezF9lm6zhT28i8si/avkMOyzNEaH9HPX6xuvV S6eg== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=date:from:to:message-id:in-reply-to:references:subject:mime-version :x-original-sender:precedence:mailing-list:list-id:list-post :list-help:list-archive:list-unsubscribe; bh=2VL3Jdu1Dns+XgkOkVt5HLwV5uieYI5WFoEiXKyvXZ8=; b=A1qihtITpViL4MH7hUVEG0yWIvZaafAJRZDFa6ov1r5pFyW8GnukhDgvuoXvhFgM8r RpjngLqywkYHuY4xeuWwWuvHiy8dGxgLLjD44csE0L7jkMfJAEgF5m6aNmT0mmAbDezU EVVEYkOXslTfjkHCPOCAQFvQYqaiVl5rsUfk+mw1G7taiFtxAoA44EN99bZgZTj/IJvC MT2mzUDqFYQer7SpKwV58H/XjCPIsU4O2emef+iYCZgzVQFE9Yr9f6WClJOI0W3JXP+z bDEUFyopnlnB+nt++mH6IyetBQio0R2vYiPXaQ+RNU62Bm1BGSDNpoJmIKix2c6plyk6 IXmw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=sender:x-gm-message-state:date:from:to:message-id:in-reply-to :references:subject:mime-version:x-original-sender:precedence :mailing-list:list-id:x-spam-checked-in-group:list-post:list-help :list-archive:list-unsubscribe; bh=2VL3Jdu1Dns+XgkOkVt5HLwV5uieYI5WFoEiXKyvXZ8=; b=HjWPtxfVR3dWFSOsex87rXBPkdjrGu6Xj009tHQAuSnw5utTh4g2cQ0CkREjqJvjh1 VQuHPv3i8cFe3uh6qcwi7v9TxAZdQUd+5oen++NgUkLEDMyg4P1alnT+eEkTsl6nWX8p lkyCVIlH5KX1F3LdVwNU+dKFjqL3kY9JFP0NfawIoqq74f+4CNSD14azZM9ENbVs6pHD G3I+pk4nbifi5NugghSmsoa9rqQr6sVfKPzF3JvrWKBJ+n/XmJXiP/F4mt2CwK/nEBXf kd3FfgUFmM9UGv5pqv7EfHVLDd2KA343RIJEXjpW2P3eh4hrJ81ix2ydpzXhENZB55yj fWhg== Sender: homotopytypetheory@googlegroups.com X-Gm-Message-State: AJcUukf9z9n2nPwCLirRQhE82Z42TgkTQx+OAUryDTaNv+Et5Dyrxl5j dh+zGKlxkMjq1rKUtuhTAlA= X-Google-Smtp-Source: ALg8bN6Qt1Gvau52gThwud1/0PG8Az3X0pk8HT8grl1x/MDcnCOGZXDilkNxy4nLNaoWd2UK9NyZnQ== X-Received: by 2002:a9d:6f9a:: with SMTP id h26mr1316989otq.0.1546909611920; Mon, 07 Jan 2019 17:06:51 -0800 (PST) X-BeenThere: homotopytypetheory@googlegroups.com Received: by 2002:a9d:2dc2:: with SMTP id g60ls1405470otb.6.gmail; Mon, 07 Jan 2019 17:06:51 -0800 (PST) X-Received: by 2002:a9d:ef3:: with SMTP id 106mr1312451otj.6.1546909611528; Mon, 07 Jan 2019 17:06:51 -0800 (PST) Date: Mon, 7 Jan 2019 17:06:50 -0800 (PST) From: Juan Ospina To: Homotopy Type Theory Message-Id: <9343db17-0282-4a4f-8701-8363317f2f8d@googlegroups.com> In-Reply-To: References: Subject: Re: [HoTT] The best proof assistant for HoTT from the point of view of automation MIME-Version: 1.0 Content-Type: multipart/mixed; boundary="----=_Part_1775_1440284747.1546909610915" X-Original-Sender: jospina65@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: , ------=_Part_1775_1440284747.1546909610915 Content-Type: multipart/alternative; boundary="----=_Part_1776_1045910795.1546909610916" ------=_Part_1776_1045910795.1546909610916 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable On Sunday, January 6, 2019 at 11:57:57 AM UTC-5, Jos=C3=A9 Manuel Rodriguez= =20 Caballero wrote: > > Hello, > After reading the (beautiful) paper=20 > > Paredes, Bel=C3=A9n. "Boson-Lattice Construction for Anyon Models." arXiv= =20 > preprint arXiv:1804.01605 (2018). > https://arxiv.org/pdf/1804.01605.pdf > > I was rather motivated to explore modular tensor categories:=20 > https://ncatlab.org/nlab/show/modular+tensor+category > > using a proof assistant. My preferred proof assistant is Isabelle/HOL,=20 > because of the hight level of automation, but I am not sure that simple= =20 > type theory is the best formal system to work with modular tensor=20 > categories. As far as I know, HoTT has been used in order to formalize=20 > category theory in a rather successful way. In my case, I programmed a=20 > little bit in UniMath (Coq), but thee automation was almost zero (maybe= =20 > there is some automation, but I did not know how to use it, everything th= at=20 > I learned in computer sciences was self-taught). > > So, I wonder in which proof assistant HoTT can be used with a maximum of= =20 > automation. > > Kind Regards, > Jos=C3=A9 M. > A trivial example of Hott with Lean=20 import homotopy.cylinder open cylinder check cylinder_rel=20 check cylinder check base check top check seg constants {A B : Type} (f : A =E2=86=92 B) constant {c : A} variables {g : A -> A} example (c : A) : base f (f (g c)) =3D top f (g c) :=3D begin rewrite seg end =20 --=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. ------=_Part_1776_1045910795.1546909610916 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Sunday, January 6, 2019 at 11:57:57 AM UTC-5, J= os=C3=A9 Manuel Rodriguez Caballero wrote:
Hello,
= =C2=A0 After reading the (beautiful) paper=C2=A0

<= div>Paredes, Bel=C3=A9n. "Boson-Lattice Construction for Anyon Models.= " arXiv preprint arXiv:1804.01605 (2018).
I was rather motivated to explore modular tensor categories:=C2= =A0

using a proof assista= nt. My preferred proof assistant is Isabelle/HOL, because of the hight leve= l of automation, but I am not sure that simple type theory is the best form= al system to work with modular tensor categories. As far as I know, HoTT ha= s been used in order to formalize category theory in a rather successful wa= y. In my case, I programmed a little bit in UniMath (Coq), but thee automat= ion was almost zero (maybe there is some automation, but I did not know how= to use it, everything that I learned in computer sciences was self-taught)= .

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

Kind Regards,=
Jos=C3=A9 M.

=


A trivial example of Hott with Lean
=


import homotopy.cylinder
open c= ylinder
check cylinder_rel
check cylinder
check base
check top=
check seg
constants {A B : Type} (f : A =E2=86=92 B)
constant {c = : A}
variables {g : A -> A}


example (c : A) : base f (f (g= c))=C2=A0 =3D top f (g c) :=3D
begin
=C2=A0 rewrite seg
end
=C2=A0

--
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.
------=_Part_1776_1045910795.1546909610916-- ------=_Part_1775_1440284747.1546909610915--