On Sunday, January 6, 2019 at 11:57:57 AM UTC-5, José Manuel Rodriguez Caballero 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. > A trivial example of Hott with Lean import homotopy.cylinder open cylinder check cylinder_rel check cylinder check base check top check seg constants {A B : Type} (f : A → B) constant {c : A} variables {g : A -> A} example (c : A) : base f (f (g c)) = top f (g c) := begin rewrite seg end -- 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.