Hello,
This is just a possible application of the conclusions in the previous discussion entitled: "[HoTT] What is knot in HOTT?"
First, I recall from the previous discussion that
André Joyal wrote:
Of course, braids, knots and tangles can be constructed algebraically
using braided monoidal categories.
The only practical quantum algorithms in order to solve decision problems belong to the class BQP (bounded-error quantum polynomial time). Indeed, a quantum algorithm which is quantum exponential in time is as useless in practice as an exponential algorithm in classical exponential time.
There is an interesting theorem [2, 3, 4] which guarantees that we only need one quantum algorithm in (quantum) polynomial time in order to solve all the BQP problems. This algorithm is the numerical evaluation of the Jones polynomial [1] of a knot at a root of unity. Indeed, any input of a BQP can be transformed into a knot in classical polynomial time, and this knot determines the solution of the original BQP problem by means of the numerical evaluation of the Jones polynomial at a root of unity.
The argument above suggests that, in place using a quantum programming language in order to solve a problem by means of an algorithm in quantum polynomial time, it is enough to focus on a classical programming language in order to transform an input into a knot in classical polynomial time and to have a fixed quantum hardware (black box) just to evaluate the Jones polynomial. I guess that such a classical programming language may be HoTT, using the Curry-Howard-Lambek correspondence (proof = algorithm = category theory).
It would be nice to know some opinions about this reduction and if it is useful in practice.
Kind Regards,
José M.
References:
[3] Freedman, Michael H., Alexei Kitaev, and Zhenghan Wang. "Simulation of topological field theories¶ by quantum computers." Communications in Mathematical Physics 227.3 (2002): 587-603. https://arxiv.org/pdf/quant-ph/0001071.pdf