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.