[HoTT] The best proof assistant for HoTT from the point of view of automation

["José Manuel Rodriguez Caballero" <josephcmac@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 1292 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 1842 bytes --]