Discussion of Homotopy Type Theory and Univalent Foundations
 help / color / mirror / Atom feed
From: Michael Shulman <shulman@sandiego.edu>
To: Langston Barrett <langston@galois.com>
Cc: "José Manuel Rodriguez Caballero" <josephcmac@gmail.com>,
	"HomotopyTypeTheory@googlegroups.com"
	<HomotopyTypeTheory@googlegroups.com>
Subject: Re: [HoTT] The best proof assistant for HoTT from the point of view of automation
Date: Mon, 7 Jan 2019 12:57:11 -0800	[thread overview]
Message-ID: <CAOvivQxW8xSdoJgo3ePoMFbk4vPv6LG0ZzAGNZSd8V4tQ=OhcQ@mail.gmail.com> (raw)
In-Reply-To: <CAJgWQArm-+HAGeCBtn_4Bw8kvfan4D8dw5+A+CUQjmgbCoguYw@mail.gmail.com>

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 <langston@galois.com> wrote:
>
> 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é Manuel Rodriguez Caballero <josephcmac@gmail.com> wrote:
>>
>> Hello,
>>   After reading the (beautiful) paper
>>
>> Paredes, Belén. "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 that 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é 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.
>
> --
> 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.

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

  reply	other threads:[~2019-01-07 20:57 UTC|newest]

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-01-06 16:57 José Manuel Rodriguez Caballero
2019-01-07 17:58 ` Langston Barrett
2019-01-07 20:57   ` Michael Shulman [this message]
2019-01-08  1:06 ` Juan Ospina
2019-01-08  1:54   ` José Manuel Rodriguez Caballero

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CAOvivQxW8xSdoJgo3ePoMFbk4vPv6LG0ZzAGNZSd8V4tQ=OhcQ@mail.gmail.com' \
    --to=shulman@sandiego.edu \
    --cc=HomotopyTypeTheory@googlegroups.com \
    --cc=josephcmac@gmail.com \
    --cc=langston@galois.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).