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.