Hello,
I am interested in the formal verification of theorems related to Quantum Computations. I have two possibilities in order to do my formalizations: either I can use simple type theory (Isabelle/HOL) or I can use UniMath (Coq). Does the homotopy type theory has some advantage over the simple type theory in this field?
Kind Regards,
José M.