SpringerLink
Log in

Topological Quantum Gates in Homotopy Type Theory

  • Published:
Communications in Mathematical Physics Aims and scope Submit manuscript

Abstract

Despite the plausible necessity of topological protection for realizing scalable quantum computers, the conceptual underpinnings of topological quantum logic gates had arguably remained shaky, both regarding their physical realization as well as their information-theoretic nature. Building on recent results on defect branes in string/M-theory (Sati and Schreiber in Rev Math Phys, 2023. https://doi.org/10.1142/S0129055X23500095. [ar**v:2203.11838]) and on their holographically dual anyonic defects in condensed matter theory (Sati and Schreiber in Rev Math Phys 35(03):2350001, 2023. https://doi.org/10.1142/S0129055X23500010. [ar**v:2206.13563]), here we explain [as announced in Sati and Schreiber (PlanQC 2022:33, 2022, [ar**v:2209.08331], [ncatlab.org/schreiber/show/Topological+Quantum+Programming+in+TED-K])] how the specification of realistic topological quantum gates, operating by anyon defect braiding in topologically ordered quantum materials, has a surprisingly slick formulation in parameterized point-set topology, which is so fundamental that it lends itself to certification in modern homotopically typed programming languages, such as cubical Agda. We propose that this remarkable confluence of concepts may jointly kickstart the development of topological quantum programming proper as well as of real-world application of homotopy type theory, both of which have arguably been falling behind their high expectations; in any case, it provides a powerful paradigm for simulating and verifying topological quantum computing architectures with high-level certification languages aware of the actual physical principles of realistic topological quantum hardware. In companion articles (Sati and Schreiber in The Quantum Monadology, [ar**v:2310.15735], Sati and Schreiber in Entanglement of Sections: The pushout of entangled and parameterized quantum information [ar**v:2309.07245]) [announced in Schreiber (Quantum types via Linear Homotopy Type Theory, talk at Workshop on Quantum Software @ QTML2022, Naples, 2022, [ncatlab.org/schreiber/files/QuantumDataInLHoTT-221117.pdf])], we explain how further passage to “dependent linear” homotopy types naturally extends this scheme to a full-blown quantum programming/certification language in which our topological quantum gates may be compiled to verified quantum circuits, complete with quantum measurement gates and classical control.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Notes

  1. Intriguingly, cohesive linear homotopy theory is also the semantic context in which to naturally make formal sense of the key ingredients of high energy physics, specifically of string/M-theory (cf. [Sc14b][

    As is usual, in (60) we are including denotation of a generic context of “constants” c of any type \(\Gamma \) – on which the execution of f may well depend, but which one may not want to regard as external parameters but as implicit arguments passed to the program (e.g. “flags”). As also usual, often we will notationally suppress this generic background context.

  2. The traditional notation for the dependent pair type is some variant of “\(\sum _{d \,:\, D} C_d\)”, pronounced the “dependent sum”. While widely used, this is clearly a misnomer—and it becomes a fatal misnomer once we generalize dependent type theory to dependent linear type theory [147), following [; alternatively one could rewrite these definitions to regard it as extra structure on . The distinction, which traditional literature glosses over anyway, is a matter of convention rather than of practical content.

  3. The inclusion (208) is of course a homomorphism of monoid (semi-group) data structures, but here we do not dwell on monoid structure, for brevity.

References

  1. Abad, C.A.: Introduction to representations of braid groups. Rev. Colomb. Mat. 49(1), 1 (2015). https://doi.org/10.15446/recolma.v49n1.54160. ar**v:1404.0724

    Article  MathSciNet  Google Scholar 

  2. Aczel, P.: On Voevodsky’s Univalence Axiom, talk at the Third European Set Theory Conference (2011), [ncatlab.org/nlab/files/Aczel-Univalence.pdf]

  3. Adamek, J., Herrlich, H., Strecker, G.: Abstract and Concrete Categories, John Wiley and Sons, New York (1990); reprinted as: Reprints in Th. Appl. Categ. 17, 1-507, (2006), [tac:tr17]

  4. Adams, J.F.: Stable homotopy and generalized homology, Chicago Lectures in Math., University of Chicago Press, 1974, [ucp:bo21302708]

  5. Adams, J.F.: Infinite Loop Spaces, Annals of Mathematics Studies, vol. 90. Princeton University Press, Princeton (1978). https://doi.org/10.1515/9781400821259

    Book  Google Scholar 

  6. Aguilar, M., Gitler, S., Prieto, C.: Algebraic Topology from a Homotopical Viewpoint. Springer, Berlin (2002). https://doi.org/10.1007/b97586

    Book  Google Scholar 

  7. Aharonov, D., van Dam, W., Kempe, J., Landau, Z., Lloyd, S., Regev, O.: Adiabatic quantum computation is equivalent to standard quantum computation, SIAM J. Comput. 37 1 (2007), 166-194

  8. Aharony, O., Gubser, S., Maldacena, J., Ooguri, H., Oz, Y.: Large \(N\) field theories, string theory and gravity. Phys. Rep. 323, 183–386 (2000). https://doi.org/10.1016/S0370-1573(99)00083-6. ar**v:hep-th/9905111

    Article  ADS  MathSciNet  Google Scholar 

  9. Ahrens, B., North, P.R.: Univalent foundations and the equivalence principle. In: Reflections on the Foundations of Mathematics, Synthese Library 407, Springer, Berlin (2019), https://doi.org/10.1007/978-3-030-15655-8, ar**v:2202.01892

  10. Ahrens, B., North, P.R., Shulman, M., Tsementzis, D.: A Higher Structure Identity Principle, LICS ‘20 (2020), 53-66, https://doi.org/10.1145/3373718.3394755, ar**v:2004.06572

  11. Aman, B., Ciobanu, G., Glück, R., Kaarsgaard, R., Kari, J., Kutrib, M., Lanese, I., Antares Mezzina, C., Mikulski, Ł., Nagarajan, R., Phillips, I., Pinna, G.M., Prigioniero, L., Ulidowski, I., Vidal, G.: Foundations of Reversible Computation, in: Reversible Computation: Extending Horizons of Computing. RC 2020, Lec. Notes Comp. Sci. 12070, Springer, New York (2020), https://doi.org/10.1007/978-3-030-47361-7_1

  12. Anderson, F.W., Fuller, K.R.: Rings and Categories of Modules, Graduate Texts in Mathematics 13 Springer. Berlin (1992). https://doi.org/10.1007/978-1-4612-4418-9

  13. Ando, M., Blumberg, A., Gepner, D., Hopkins, M., Rezk, C.: An \(\infty \)-categorical approach to \(R\)-line bundles, R\(R\)-module Thom spectra, and twisted \(R\)-homology. J. Topology 7(3), 869–893 (2014)

    Article  MathSciNet  Google Scholar 

  14. Arkowitz, M.: Introduction to Homotopy Theory. Springer, Berlin (2011). https://doi.org/10.1007/978-1-4419-7329-0

    Book  Google Scholar 

  15. Artin, E.: Theorie der Zöpfe. Abh. Math. Semin. Univ. Hambg. 4, 47–72 (1925). https://doi.org/10.1007/BF02950718

    Article  Google Scholar 

  16. Avron, J.E., Seiler, R., Yaffe, L.G.: Adiabatic theorems and applications to the quantum Hall effect. Commun. Math. Phys. 110, 33–49 (1987). https://doi.org/10.1007/BF01209015

    Article  ADS  MathSciNet  Google Scholar 

  17. Awodey, S.: Type theory and homotopy, In: Epistemology versus Ontology, Springer, Berlin (2012), 183-201, https://doi.org/10.1007/978-94-007-4435-6_9, ar**v:1010.1810

  18. Awodey, S.: Natural Models of Homotopy Type Theory (Abstract). in: Logic, Language, Information, and Computation. WoLLIC 2013. Lecture Notes in Computer Science 8071, Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39992-3_2ar**v:1406.3219 (2013)

  19. Awodey, S., Bauer, A.: Propositions as [Types]. J. Logic Comput. 14, 447–471 (2004). https://doi.org/10.1093/logcom/14.4.447

    Article  MathSciNet  Google Scholar 

  20. Awodey, S., Gambino, N., Sojakova, K.: Inductive types in homotopy type theory, LICS’12 (2012), 95-104, https://doi.org/10.1109/LICS.2012.21, ar**v:1201.3898

  21. Awodey, S., Gambino, N., Sojakova, K.: Homotopy-initial algebras in type theory. J. Assoc. Comput. Mach. 636, 1–45 (2017). https://doi.org/10.1145/3006383. ar**v:1504.05531

    Article  Google Scholar 

  22. Awodey, S., Warren, M.: Homotopy theoretic models of identity type. Math. Proc. 146, 45–55 (2009). https://doi.org/10.1017/S0305004108001783. ar**v:0709.0248

    Article  MathSciNet  Google Scholar 

  23. Bachmann, S., De Roeck, W., Fraas, M.: The adiabatic theorem in a quantum many-body setting. In: Analytic Trends in Mathematical Physics, Cont. Math. 741, 43-58, (2020), [ams:conm-741], ar**v:1808.09985

  24. Bailey, D., Borwein, P., Plouffe, S.: On the rapid computation of various polylogarithmic constants. Math. Comp. 66, 903–913 (1997)

    Article  ADS  MathSciNet  Google Scholar 

  25. Balmer, P.: Stacks of group representations. J. Eur. Math. Soc. 17(1), 189–228 (2015). https://doi.org/10.4171/jems/501. ar**v:1302.6290

    Article  MathSciNet  Google Scholar 

  26. Barthe, G., Capretta, V., Pons, O.: Setoids in type theory. J. Funct. Progr. 13(2), 261–293 (2003). https://doi.org/10.1017/S0956796802004501

    Article  MathSciNet  Google Scholar 

  27. Barthe, G., Pons, O.: Type Isomorphisms and Proof Reuse in Dependent Type Theory, in: Foundations of Software Science and Computation Structures. FoSSaCS 2001, Lecture Notes in Computer Science 2030, Springer, Berlin (2001), https://doi.org/10.1007/3-540-45315-6_4

  28. Baues, H.J.: Homotopy Types in Handbook of Algebraic Topology, North Holland (1995), 1-72, https://doi.org/10.1016/B978-0-444-81779-2.X5000-7, [ncatlab.org/nlab/files/Baues-HomotopyTypes.pdf]

  29. Benenti, G., Casati, G., Rossini, D.: Principles of Quantum Computation and Information, World Scientific, Singapore (2004, 2018), https://doi.org/10.1142/10909

  30. Benioff, P.: The computer as a physical system: a microscopic quantum mechanical Hamiltonian model of computers as represented by Turing machines. J. Stat. Phys. 22, 563–591 (1980). https://doi.org/10.1007/BF01011339

    Article  ADS  MathSciNet  Google Scholar 

  31. Bennett, C.H.: Notes on Landauer’s principle, reversible computation, and Maxwell’s Demon. Stud. Hist. Philos. Mod. Phys. 34(3), 501–510 (2003). https://doi.org/10.1016/S1355-2198(03)00039-X

    Article  MathSciNet  Google Scholar 

  32. Berry, M.V.: Quantal phase factors accompanying adiabatic changes. Proc. R. Soc. Lond. A 392, 45–57 (1984). https://doi.org/10.1098/rspa.1984.0023

    Article  ADS  MathSciNet  Google Scholar 

  33. Berry, M.: The quantum phase, five years after, In: Geometric phases in physics, Adv. Ser. Math. Phys. 5, World Scientific (1989), 7–28, https://doi.org/10.1142/0613

  34. Bezem, M., Buchholtz, U., Cagne, P., Dundas, B.I., Grayson, D.R.: Symmetry (2021), [unimath.github.io/SymmetryBook/book.pdf], [github.com/UniMath/agda-unimath/tree/master/src/group-theory]

  35. Birkhoff, G., von Neumann, J.: The logic of quantum mechanics. Ann. Math. 37, 823–843 (1936). https://doi.org/10.2307/1968621

    Article  MathSciNet  Google Scholar 

  36. Birman, J.S.: Braids, Links, and Map** Class Groups. Princeton University Press, Princeton (1975)

    Book  Google Scholar 

  37. Bishop, E.: Foundations of Constructive Analysis, McGraw-Hill (1967), [archive.org/details/foundationsofcon0000bish]

  38. Bishop, E., Bridges, D.: Constructive Analysis, vol. 279. Springer, Berlin (1985). https://doi.org/10.1007/978-3-642-61667-9

    Book  Google Scholar 

  39. Bland, P.E.: Rings and Their Modules. De Gruyter. Berlin (2011). https://doi.org/10.1515/9783110250237

  40. Bohannon, A., Pierce, B.C., Vaughan, J.A.: Relational lenses: a language for updatable views, Proceedings of Principles of Database Systems (2006), 338-347, https://doi.org/10.1145/1142351.1142399

  41. Bonesteel, N.E., Hormozi, L., Zikos, G., Simon, S.H.: Braid topologies for quantum computation. Phys. Rev. Lett. 95, 140503 (2005). https://doi.org/10.1103/PhysRevLett.95.140503. [ar**v:quant-ph/0505065]

    Article  ADS  MathSciNet  Google Scholar 

  42. Booth, P.I.: The Exponential Law of Maps I, Proc. London Math. Soc. s3-20 (1970), 179-192, https://doi.org/10.1112/plms/s3-20.1.179

  43. Booth, P.I., Brown, R.: Spaces of partial maps, fibred map** spaces and the compact-open topology. Gen. Topol. Appl. 8, 181–195 (1978). https://doi.org/10.1016/0016-660X(78)90049-1

    Article  MathSciNet  Google Scholar 

  44. Borceux, F.: Categories and Structures, Vol. 2 of: Handbook of Categorical Algebra, Enc. Math. Appl., vol. 50. Cambridge University Press, Cambridge (1994). https://doi.org/10.1017/CBO9780511525865

    Book  Google Scholar 

  45. Borceux, F.: Categories of Sheaves, Vol. 3 of: Handbook of Categorical Algebra, Enc. Math. Appl., vol. 50. Cambridge University Press, Cambridge (1994). https://doi.org/10.1017/CBO9780511525872

    Book  Google Scholar 

  46. Bouwmeester, D., Ekert, A., Zeilinger, A.: The Physics of Quantum Information-Quantum Cryptography, Quantum Teleportation, Quantum Computation. Springer, New York (2020). https://doi.org/10.1007/978-3-662-04209-0

  47. Braunack-Mayer, V.: Combinatorial parametrised spectra. Algebr. Geom. Topol. 21, 801–891 (2021). https://doi.org/10.2140/agt.2021.21.801. [ar**v:1907.08496]

    Article  MathSciNet  Google Scholar 

  48. Bredon, G.: Topology and Geometry, Graduate Texts in Math. 139, Springer, Berlin (1993), https://doi.org/10.1007/978-1-4757-6848-0

  49. Brennen, G.K., Pachos, J.K.: Why should anyone care about computing with anyons? Proc. R. Soc. A 464, 1–24 (2008). https://doi.org/10.1098/rspa.2007.0026. [ar**v:0704.2241]

    Article  ADS  MathSciNet  Google Scholar 

  50. Bridges, D.: Constructive mathematics: a foundation for computable analysis. Theor. Comp Sci. 219(1–2), 95–109 (1999). https://doi.org/10.1016/S0304-3975(98)00285-0

    Article  MathSciNet  Google Scholar 

  51. Brown, E.H., Jr.: Abstract homotopy theory. Trans. Am. Math. Soc. 119, 79–85 (1965). https://doi.org/10.1090/S0002-9947-1965-0182970-6

    Article  MathSciNet  Google Scholar 

  52. Brown, K.S.: Abstract Homotopy Theory and Generalized Sheaf Cohomology, Trans. Amer. Math. Soc., 186, 419-458, (1973) [jstor:1996573]

  53. Brunekreef, J.W.: Topological Quantum Computation and Quantum Compilation, thesis, Utrecht (2014), [studentheses:20.500.12932/17738]

  54. Brunerie, G., Licata, D., Lumsdaine, P.: Homotopy theory in type theory, lecture notes (2013), [dlicata.wescreates.wesleyan.edu/pubs/bll13homotopy/bll13homotopy.pdf]

  55. Brunerie, G., Ljungström, A., Mörtberg, A.: Synthetic Integral Cohomology in Cubical Agda. In: 30th EACSL Annual Conference on Computer Science Logic (CSL 2022) 216 (2022), https://doi.org/10.4230/LIPIcs.CSL.2022.11

  56. Buchholtz, U., Christensen, J.D., Taxerás Flaten, J., Rijke, E.: Central H-spaces and banded types, [ar**v:2301.02636]

  57. Buchholtz, U., van Doorn, F., Rijke, E.: Higher groups in homotopy type theory. LICS 33, 205–214 (2018). https://doi.org/10.1145/3209108.3209150. [ar**v:1802.04315]

    Article  Google Scholar 

  58. Bunge, M.: Possibility and Probability. In: Foundations of Probability Theory, Statistical Interference, and Statistical Theories of Science, Reidel Publishing, pp. 17-34 (1976), https://doi.org/10.1007/978-94-010-1438-0_2

  59. Bunke, U., Nikolaus, T., Völkl, M.: Differential cohomology theories as sheaves of spectra. J. Homotopy Rel. Struct. 11, 1–66 (2016). https://doi.org/10.1007/s40062-014-0092-5. [ar**v:1311.3188]

    Article  MathSciNet  Google Scholar 

  60. Cabra, D.C., Rossini, G.L.: Explicit connection between conformal field theory and 2+1 Chern-Simons theory. Mod. Phys. Lett. A 12, 1687–1697 (1997). https://doi.org/10.1142/S0217732397001722. [ar**v:hep-th/9506054]

    Article  ADS  MathSciNet  Google Scholar 

  61. Cagliari, F., Mantovani, S., Vitale, E.: Regularity of the category of Kelley spaces. Appli. Categ. Struc. 3, 357–361 (1995). https://doi.org/10.1007/BF00872904

    Article  MathSciNet  Google Scholar 

  62. Cattaneo, A., Giaquinto, A., Xu, P.: Higher Structures in Geometry and Physics - In Honor of Murray Gerstenhaber and Jim Stasheff, Progress in Mathematics 287. Birkhäuser (2001). https://doi.org/10.1007/978-0-8176-4735-3

    Article  Google Scholar 

  63. Cavallo, E.: Synthetic Cohomology in Homotopy Type Theory., PhD Thesis, Carnegie Mellon University (2015), [staff.math.su.se/evan.cavallo/works/thesis15.pdf]

  64. Cesare, C., Landahl, A.J., Bacon, D., Flammia, S.T., Neels, A.: Adiabatic topological quantum computing. Phys. Rev. A 92, 012336 (2015). https://doi.org/10.1103/PhysRevA.92.012336. [ar**v:1406.2690]

    Article  ADS  Google Scholar 

  65. Cheng, M., Galitski, V., Das Sarma, S.: Non-adiabatic Effects in the Braiding of Non-Abelian Anyons in Topological Superconductors. Phys. Rev. B 84, 104529 (2011)

    Article  ADS  Google Scholar 

  66. Cherubini, F., Rijke, E.: Modal descent. Math. Struc. Comput. Sci. 31, 4 (2021)

    Article  MathSciNet  Google Scholar 

  67. Childs, A., Farhi, E., Preskill, J.: Robustness of adiabatic quantum computation. Phys. Rev. A 65, 012322 (2002). https://doi.org/10.1103/PhysRevA.65.012322. [ar**v:quant-ph/0108048]

    Article  ADS  Google Scholar 

  68. Chlipala, A.: Implementing Certified Programming Language Tools in Dependent Type Theory, PhD thesis, U. California at Berkeley (2007), [UCB/EECS-2007-113]

  69. Chlipala, A.: Certified programming with dependent types, MIT Press, Boston (2013), [ISBN:9780262026659]

  70. Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5(2), 56–68 (1940). https://doi.org/10.2307/2266170

    Article  MathSciNet  Google Scholar 

  71. Cisinski, D.-C.: Cambridge University Press. (2019). https://doi.org/10.1017/9781108588737

  72. Clarke, J., Wilhelm, F.K.: Superconducting quantum bits. Nature 453, 1031–1042 (2008). https://doi.org/10.1038/nature07128

    Article  ADS  Google Scholar 

  73. Coen, C.S., Tassi, E.: Working with Mathematical Structures in Type Theory, in: Types for Proofs and Programs. TYPES 2007, Lecture Notes in Computer Science 4941 Springer (2008), https://doi.org/10.1007/978-3-540-68103-8_11

  74. Cohen, F.R.: Introduction to configuration spaces and their applications, In: Braids, Lecture Notes Series, Institute for Mathematical Sciences, 19, 183–261. World Scientific, Singapore (2009)

  75. Cohen, C., Coquand, T., Huber, S., Mörtberg, A.: Cubical Type Theory: a constructive interpretation of the univalence axiom, 21st International Conference on Types for Proofs and Programs (TYPES 2015), 5.1-5.34, Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany https://doi.org/10.48550/ar**v.1611.02108

  76. Coquand, T.: Equality and dependent type theory, lecture notes (2011), [ncatlab.org/nlab/files/Coquand-EqualityAndDependentTypeTheory.pdf]

  77. Coquand, T., Danielsson, N.A.: Isomorphism is equality. Indag. Math. 24(4), 1105–1120 (2013). https://doi.org/10.1016/j.indag.2013.09.002

    Article  MathSciNet  Google Scholar 

  78. Coquand, Thierry, Huber, Simon, Mörtberg, Anders: On Higher Inductive Types in Cubical Type Theory, in Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS ’18) (2018), Association for Computing Machinery, New York, NY, USA, pp. 255–264. https://doi.org/10.1145/3209108.3209197

  79. Coquand, T., Paulin, C.: Inductively defined types, COLOG-88 Lecture Notes in Computer Science 417, Springer, Berlin (1990), pp. 50-66, https://doi.org/10.1007/3-540-52335-9_47

  80. Coquand, T., Spiwack, A.: Towards constructive homological algebra in type theory, in: Towards Mechanized Mathematical Assistants. MKM Calculemus 2007, Lecture Notes in Computer Science 4573 Springer, Berlin (2007), https://doi.org/10.1007/978-3-540-73086-6_4

  81. O’Connor, R., Monadic, A.: Functional Implementation of Real Numbers. Math. Struc. Comput. Sci. 17(1), 129–159 (2007). https://doi.org/10.1017/S0960129506005871. [ar**v:cs/0605058]

    Article  MathSciNet  Google Scholar 

  82. Constable, R.: The Triumph of Types: Creating a Logic of Computational Reality, lecture at: Types, Semantics and Verification, Oregon (2011), [www.cs.uoregon.edu/research/summerschool/summer11/lectures/Triumph-of-Types-Extended.pdf]

  83. Corfield, D., Sati, H., Schreiber, U.: Fundamental weight systems are quantum states, [ar**v:2105.02871]

  84. Corry, L.: Modern Algebra and the Rise of Mathematical Structures. Springer. Berlin (2004). https://doi.org/10.1007/978-3-0348-7917-0

    Article  MathSciNet  Google Scholar 

  85. Corry, L.: A Brief History of Numbers, Oxford University Press (2015), [ISBN:9780198702597]

  86. Cory, D.G., Laflamme, R., Knill, E., Viola, L., Havel, T.F., Boulant, N., Boutis, G., Fortunato, E., Lloyd, S., Martinez, R., Negrevergne, C., Pravia, M., Sharf, Y., Teklemariam, G., Weinstein, Y.S., Zurek, W.H.: NMR Based Quantum Information Processing: Achievements and Prospects, Fortsch. Phys. 48 (2000), 875-907, [ar**v:quant-ph/0004104], https://doi.org/10.1002/1521-3978(200009)48:9/11\(<\)875::AID-PROP875\(>\)3.0.CO;2-V

  87. Crabb, M.C., James, I.M.: Fiberwise Homotopy Theory. Springer, Berlin (1998). https://doi.org/10.1007/978-1-4471-1265-5

  88. Curien, P.-L., Garner, R., Hofmann, M.: Revisiting the categorical interpretation of dependent type theory. Theor. Comput. Sci. 546(21), 99–119 (2014). https://doi.org/10.1016/j.tcs.2014.03.003

    Article  MathSciNet  Google Scholar 

  89. Das Sarma, S.: Quantum computing has a hype problem, MIT Technology Review (March 2022), [www.technologyreview.com/2022/03/28/1048355/quantum-computing-has-a-hype-problem]

  90. Das Sarma, S.: In search of Majorana, [ar**v:2210.17365]

  91. Das Sarma, S., Pan, H.: Disorder-induced zero-bias peaks in Majorana nanowires, Phys. Rev. B 103 (2021) 195158, https://doi.org/10.1103/PhysRevB.103.195158, [ar**v:2103.05628]

  92. Date, E., Jimbo, M., Matsuo, A., Miwa, T.: Hypergeometric-type integrals and the \(\mathfrak{sl} (2,\mathbb{C} )\) Knizhnik-Zamolodchikov equation. Int. J. Mod. Phys. B 4(5), 1049–1057 (1990). https://doi.org/10.1142/S0217979290000528

    Article  ADS  Google Scholar 

  93. Dawson, C.M., Nielsen, M.A.: The Solovay-Kitaev algorithm. Quantum Info. Comput. 6(1), 81–95 (2006). https://doi.org/10.5555/2011679.2011685. [ar**s in typed lambda calculus. Inf. Comput. 91(2), 189–204 (1991). https://doi.org/10.1016/0890-5401(91)90066-B

    Article  MathSciNet  Google Scholar 

  94. Deligne, P.: Equations différentielles à points singuliers règuliers, Lect. Notes Math. 163 Springer (1970), [ias:355]

  95. Deutsch, D.E.: Quantum computational networks. Proc. R. Soc. A 425(1868), 73–90 (1989). https://doi.org/10.1098/rspa.1989.0099

    Article  ADS  MathSciNet  Google Scholar 

  96. Di Cosmo, R.: Isomorphisms of Types - from \(\lambda \)-calculus to information retrieval and language design. Progress Theor. Comput. Sci. (1995). https://doi.org/10.1007/978-1-4612-2572-0

    Article  Google Scholar 

  97. Di Francesco, P., Mathieu, P., Sénéchal, D.: Conformal Field Theory. Springer, Berlin (1997). https://doi.org/10.1007/978-1-4612-2256-9

    Book  Google Scholar 

  98. Dimca, A.: Sheaves in Topology. Springer, Berlin (2004). https://doi.org/10.1007/978-3-642-18868-8

    Book  Google Scholar 

  99. Ding, M., Roberts, C.D., Schmidt, S.M.: Emergence of Hadron Mass and Structure, [ar**v:2211.07763]

  100. Downen, P., Ariola, Z.M.: A tutorial on computational classical logic and the sequent calculus. J. Funct. Progr. 28, E3 (2018). https://doi.org/10.1017/S0956796818000023

    Article  MathSciNet  Google Scholar 

  101. Dowling, M.R., Nielsen, M.A.: The geometry of quantum computation. Quant. Info. Comput. 8(10), 861–899 (2008). https://doi.org/10.5555/2016985.2016986. [ar**v:quant-ph/0701004]

    Article  MathSciNet  Google Scholar 

  102. Duff, M.: The World in Eleven Dimensions: Supergravity, Supermembranes and M-theory, IoP, Bristol (1999), [ISBN:9780750306720]

  103. Dwyer, W., Spalinski, J.: Homotopy theories and model categories. In: I. M. James (ed.), Handbook of Algebraic Topology, North Holland (1995), https://doi.org/10.1016/B978-0-444-81779-2.X5000-7

  104. Dybjer, P.: Inductive families. Formal Aspects Comput. 6, 440–465 (1994). https://doi.org/10.1007/BF01211308

    Article  Google Scholar 

  105. Dybjer, P.: Internal Type Theory, Types for Proofs and Programs. TYPES 1995. Lecture Notes in Computer Science 1158 Springer (1995) https://doi.org/10.1007/3-540-61780-9_66

  106. Dybjer, P.: Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. Theor. Comput. Sci. 176(1–2), 329–335 (1997). https://doi.org/10.1016/S0304-3975(96)00145-4

    Article  MathSciNet  Google Scholar 

  107. Equbal, A.: Molecular spin qubits for future quantum technology, Quantum Colloquium at CQTS (Nov 2022), [ncatlab.org/nlab/show/CQTS#EqubalNov22]

  108. Erlich, J.: An Introduction to Holographic QCD for Nonspecialists. Contemp. Phys. 56, 2 (2015). [ar**v:1407.5002]

    Article  Google Scholar 

  109. Escardó, M.H.: Introduction to Univalent Foundations of Mathematics with Agda (2019), [ar**v:1911.00580], [cs.bham.ac.uk/\(\sim \)mhe/HoTT-UF-in-Agda-Lecture-Notes]

  110. Etingof, P.I., Frenkel, I., Kirillov, A.A.: Lectures on Representation Theory and Knizhnik-Zamolodchikov Equations, Math. Surv. monogr. 58, Amer. Math. Soc., Providence, RI (1998), [ams.org/surv-58]

  111. Fadell, E., Neuwirth, L.: Configuration spaces. Math. Scand. 10, 111–118 (1962). https://doi.org/10.7146/math.scand.a-10517

    Article  MathSciNet  Google Scholar 

  112. Fadell, E., Husseini, S.: Geometry and topology of configuration spaces. Springer, Berlin (2001). https://doi.org/10.1007/978-3-642-56446-8

  113. Farhi, E., Goldstone, J., Gutmann, S., Sipser, M.: Quantum Computation by Adiabatic Evolution, [ar**v:quant-ph/0001106]

  114. Feynman, R.: Simulating physics with computers. Int. J. Theor. Phys. 21, 467–488 (1982). https://doi.org/10.1007/BF02650179

    Article  MathSciNet  Google Scholar 

  115. Feigin, B., Schechtman, V., Varchenko, A.: On algebraic equations satisfied by hypergeometric correlators in WZW models. I, Commun. Math. Phys. 163 (1994), 173-184, https://doi.org/10.1007/BF02101739

  116. Fiorenza, D., Sati, H., Schreiber, U.: The rational higher structure of M-theory. Fortsch. Phys. 67, 1910017 (2019). https://doi.org/10.1002/prop.201910017. [ar**v:1903.02834]

    Article  ADS  MathSciNet  Google Scholar 

  117. Fiorenza, D., Sati, H., Schreiber, U.: The Character Map in Non-Abelian Cohomology-Twisted, Differential and Generalized. World Scientific (2023). https://doi.org/10.1142/13422. [ar**v:2009.11909]

    Article  Google Scholar 

  118. Fox, R.H., Neuwirth, L.: The braid groups. Math. Scand. 10, 119–126 (1962). https://doi.org/10.7146/math.scand.a-10518

    Article  MathSciNet  Google Scholar 

  119. Freed, D.S., Moore, G.W.: Twisted equivariant matter. Ann. Henri Poincaré 14, 1927–2023 (2013). https://doi.org/10.1007/s00023-013-0236-x. [ar**v:1208.5055]

    Article  ADS  MathSciNet  Google Scholar 

  120. Freedman, M.: P/NP, and the quantum field-computer. Proc. Nat. Acad. Sci. 95(1), 98–101 (1998). https://doi.org/10.1073/pnas.95.1.9

    Article  ADS  MathSciNet  Google Scholar 

  121. Freedman, M.H., Larsen, M., Wang, Z.: A modular functor which is universal for quantum computation. Commun. Math. Phys. 227, 605–622 (2002). https://doi.org/10.1007/s002200200645. [ar**v:quant-ph/0001108]

    Article  ADS  MathSciNet  Google Scholar 

  122. Freedman, M., Kitaev, A., Larsen, M., Wang, Z.: Topological Quantum Computation. Bull. Am. Math. Soc. 40, 31 (2003). https://doi.org/10.1090/S0273-0979-02-00964-3. [ar**v:quant-ph/0101025]

    Article  MathSciNet  Google Scholar 

  123. Frege, G.: Begriffsschrift:eine der arithmetischen nachgebildete Formelsprache des reinen Denkens, Verlag von Louis Nebert (1879), [ISBN:9783487006239]; English translation: J. Corcoran and D. Levin, Gottlob Frege: Conceptual notation and related articles, Oxford University Press (1972), https://doi.org/10.1086/288549

  124. Fuchs, L.: Abelian Groups. Springer. Berlin (2015). https://doi.org/10.1007/978-3-319-19422-6

  125. Gaitsgory, D., Lurie, J.: Weil’s conjecture for function fields (2014-2017), [www.math.ias.edu/\(\sim \)lurie/papers/tamagawa-abridged.pdf]

  126. Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging Mathematical Structures, in: Theorem Proving in Higher Order Logics. TPHOLs 2009, Lecture Notes in Computer Science 5674 Springer, Berlin (2009), https://doi.org/10.1007/978-3-642-03359-9_23

  127. Gawedzki, K.: Conformal field theory: a case study, in Conformal Field Theory-New Non-perturbative Methods in String and Field Theory. CRC Press (2000). https://doi.org/10.1201/9780429502873. [ar**v:hep-th/9904145]

    Article  Google Scholar 

  128. Gell-Mann, M.: The interpretation of the new particles as displaced charge multiplets. Nuovo Cim 4(2), 848–866 (1956). https://doi.org/10.1007/BF02748000

    Article  ADS  MathSciNet  Google Scholar 

  129. Gentzen, G.: Untersuchungen über das logische Schließen. Math. Zeitschrift 39, 176–210 (1935). https://doi.org/10.1007/BF01201353

    Article  MathSciNet  Google Scholar 

  130. Gentzen, G.: Investigations into Logical Deduction, translated by M. E. Szabo (ed.) in: The Collected Papers of Gerhard Gentzen, Studies in Logic and the Foundations of Mathematics 55, Springer, Berlin (1969), 68-131, [ISBN:9780444534194]

  131. Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Struc. Comput. Sci. 17(01), 3–36 (2007). https://doi.org/10.1017/S0960129506005834

    Article  MathSciNet  Google Scholar 

  132. Goerss, P., Jardine, J.F.: Simplicial Homotopy Theory, Progress in Mathematics. Birkhäuser. Boston (2009). https://doi.org/10.1007/978-3-0346-0189-4

  133. Götz, L.: Martin-Löf’s J-rule, Bachelor’s Thesis, Ludwig Maximili an Univ., Munich, 2018, [math.lmu.de/\(\sim \)petrakis/Goetz.pdf]

  134. Golze, D., Icker, M., Berger, S.: Implementation of two-qubit and three-qubit quantum computers using liquid-state nuclear magnetic resonance. Concepts Mag. Resonance 40A(1), 25–37 (2012). https://doi.org/10.1002/cmr.a.21222

    Article  Google Scholar 

  135. Govzmann, A., Pištalo, D., Poncin, N.: Indeterminacies and models of homotopy limits, [ar**v:2109.12395]

  136. Grady, D., Sati, H.: Twisted differential \({{\rm KO}} \)-theory, [ar**v:1905.09085]

  137. Grant, E.K., Humble, T.S.: Adiabatic Quantum Computing and Quantum Annealing. Oxford Research Encyclopedia (2020). https://doi.org/10.1093/acrefore/9780190871994.013.32

  138. Griffiths, P.A.: Periods of integrals on algebraic manifolds: summary of main results and discussion of open problems. Bull. Am. Math. Soc. 76, 228–296 (1970). https://doi.org/10.1090/S0002-9904-1970-12444-2

    Article  MathSciNet  Google Scholar 

  139. Grothendieck, A.: On the de Rham cohomology of algebraic varieties, Inst. Hautes Études Sci. Publ. Math. 29 (1966), 95-103

  140. Gu, X., Haghighat, B., Liu, Y.: Ising- and Fibonacci-Anyons from KZ-equations. J. High Energy Phys. 2022, 15 (2022). https://doi.org/10.1007/JHEP09(2022)015. [ar**v:2112.07195]

    Article  MathSciNet  Google Scholar 

  141. Gunter, C.A.: The Semantics of Types in Programming Languages, in: Handbook of Logic in Computer Science, Vol 3: Semantic structures, Oxford University Press (1995), [ISBN:9780198537625]

  142. Hardie, K.A., Kamps, K.H., Kieboom, R.: A homotopy bigroupoid of a topological space. Appl. Categ. Struct. 9, 311–327 (2001). https://doi.org/10.1023/A:1011270417127

    Article  MathSciNet  Google Scholar 

  143. Harper, R.: Practical Foundations for Programming Languages, Cambridge University Press (2016), [ISBN:9781107150300]

  144. Hartnoll, S., Lucas, A., Sachdev, S.: Holographic quantum matter, MIT Press, Boston, (2018), [ISBN:9780262348010], [ar**v:1612.07324]

  145. Hatcher, A.: Algebraic Topology, Cambridge University Press (2002) [ISBN:9780521795401], [https://pi.math.cornell.edu/~hatcher/AT/ATpage.html]

  146. Hilton, P.: Subjective history of homology and homotopy theory. Math. Mag. 61(5), 282–291 (1988). https://doi.org/10.2307/2689545

    Article  MathSciNet  Google Scholar 

  147. Hofmann, M.: Extensional concepts in intensional type theory, Ph.D. thesis, Edinburgh (1995), Distinguished Dissertations, Springer (1997), [ECS-LFCS-95-327],https://doi.org/10.1007/978-1-4471-0963-1

  148. Hofmann, M.: Syntax and semantics of dependent types, in: Semantics and logics of computation, Publ. Newton Inst. 14, Cambridge University Press (1997), pp. 79-130, https://doi.org/10.1017/CBO9780511526619.004

  149. Hofmann, M., Streicher, T.: The groupoid interpretation of type theory. In: Twenty-five years of constructive type theory, Oxf. Logic Guides. 36, Clarendon Press (1998), pp. 83–111, [ISBN:9780198501275]

  150. Hormozi, L., Bonesteel, N.E., Simon, S.H.: Topological quantum computing with Read-Rezayi states. Phys. Rev. Lett. 103, 160501 (2009). https://doi.org/10.1103/PhysRevLett.103.160501. [ar**v:0903.2239]

    Article  ADS  MathSciNet  Google Scholar 

  151. Hormozi, L., Zikos, G., Bonesteel, N.E., Simon, S.H.: Topological quantum compiling. Phys. Rev. B 75, 165310 (2007). https://doi.org/10.1103/PhysRevB.75.165310. [ar**v:quant-ph/0610111]

    Article  ADS  Google Scholar 

  152. Hou, K.-B., Finster, E., Licata, D., Lumsdaine, P.: A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory, LICS ‘16 (2016), pp. 565–574, https://doi.org/10.1145/2933575.2934545, [ar**v:1605.03227]

  153. Huang, H.-L., Wu, D., Fan, D., Zhu, X.: Superconducting quantum computing: a review. Sci. China Inf. Sci. 63(8), 1–32 (2020). https://doi.org/10.1007/s11432-020-2881-9. [ar**v:2006.10433]

    Article  ADS  MathSciNet  Google Scholar 

  154. Jacobs, B.: Comprehension categories and the semantics of type dependency. Theor. Comput. Sci. 107(2), 169–207 (1993). https://doi.org/10.1016/0304-3975(93)90169-T

    Article  MathSciNet  Google Scholar 

  155. Jacobs, B.: Categorical Logic and Type Theory, Studies in Logic and the Foundations of Mathematics 141, Elsevier (1998), [ISBN:9780444501707]

  156. James, I.M.: General Topology and Homotopy Theory. Springer. Berlin (1984). https://doi.org/10.1007/978-1-4613-8283-6

  157. Jänich, K.: Topology, Undergraduate Texts in Mathematics, Springer, Berlin (1984), [ISBN:9780387908922]

  158. Johansen, E.G., Simula, T.: Fibonacci anyons versus Majorana fermions-A Monte Carlo Approach to the Compilation of Braid Circuits in \({{\rm SU}}(2)_k\) Anyon Models. PRX Quantum 2, 010334 (2021). https://doi.org/10.1103/PRXQuantum.2.010334. [ar**v:2008.10790]

    Article  Google Scholar 

  159. Johnson, D.L.: Presentations of Groups. Cambridge University Press, Cambridge (1990)

    Google Scholar 

  160. Joyal, A.: Notes on Clans and Tribes, [ar**v:1710.10238]

  161. Jurčo, B., Saemann, C., Schreiber, U., Wolf, M.: Higher structures in M-theory. Fortsch. Phys. 67, 8–9 (2019)

    MathSciNet  Google Scholar 

  162. Kachapova, F.: Formalizing groups in type theory, [ar**v:2102.09125]

  163. Kadowaki, T., Nishimori, H.: Quantum annealing in the transverse Ising model. Phys. Rev. E 58, 5355–5363 (1998). https://doi.org/10.1103/PhysRevE.58.5355. [ar**v:cond-mat/9804280]

    Article  ADS  Google Scholar 

  164. Kamps, K.H., Porter, T.: Abstract Homotopy and Simple Homotopy Theory. World Scientific, Singapore (1997)

    Book  Google Scholar 

  165. Kapulkin, C., LeFanu Lumsdaine, P., Voevodsky, V.: Univalence in simplicial sets, [ar**v:1203.2553]

  166. Kapulkin, C., LeFanu Lumsdaine, P.: The simplicial model of univalent foundations (after Voevodsky). J. Eur. Math. Soc. 23, 2071–2126 (2021)

    Article  MathSciNet  Google Scholar 

  167. Katz, N.M.: On the differential equations satisfied by period matrices. Inst. Hautes Études Sci. Publ. Math. 35, 223–258 (1968)

    Article  MathSciNet  Google Scholar 

  168. Katz, N.M., Oda, T.: On the differentiation of de Rham cohomology classes with respect to parameters. J. Math. Kyoto Univ. 8, 199–213 (1968). https://doi.org/10.1215/kjm/1250524135

    Article  MathSciNet  Google Scholar 

  169. Kauffman, L.H., Lomonaco, S.J., Jr.: Braiding operators are universal quantum gates. New J. Phys. 6, 134 (2004). https://doi.org/10.1088/1367-2630/6/1/134. [ar**v:quant-ph/0401090]

    Article  ADS  Google Scholar 

  170. Kitaev, A.: Quantum computations: algorithms and error correction. Russian Math. Surv. 52, 1191–1249 (1997). https://doi.org/10.1070/rm1997v052n06abeh002155

    Article  ADS  MathSciNet  Google Scholar 

  171. Kitaev, A.: Unpaired Majorana fermions in quantum wires. Phys. Usp. 44(131), 131–136 (2001). https://doi.org/10.1070/1063-7869/44/10S/S29. [ar**v:cond-mat/0010440]

    Article  ADS  Google Scholar 

  172. Kitaev, A.: Fault-tolerant quantum computation by anyons. Ann. Phys. 303, 2–30 (2003). https://doi.org/10.1016/S0003-4916(02)00018-0. [ar**v:quant-ph/9707021]

    Article  ADS  MathSciNet  Google Scholar 

  173. Kitaev, A.: Anyons in an exactly solved model and beyond. Ann. Phys. 321(1), 2–111 (2006). https://doi.org/10.1016/j.aop.2005.10.005. [ar**v:cond-mat/0506438]

    Article  ADS  MathSciNet  Google Scholar 

  174. Kitaev, A.: Periodic table for topological insulators and superconductors. AIP Conf. Proc. 1134, 22 (2009). https://doi.org/10.1063/1.3149495. [ar**v:0901.2686]

    Article  ADS  Google Scholar 

  175. Kliuchnikov, V., Bocharov, A., Svore, K.M.: Asymptotically optimal topological quantum compiling. Phys. Rev. Lett. 112, 140504 (2014). https://doi.org/10.1103/PhysRevLett.112.140504. [ar**v:1310.4150]

    Article  ADS  Google Scholar 

  176. Knapp, A.: Basic Algebra. Springer, Berlin (2006)

    Book  Google Scholar 

  177. Knill, E.: Conventions for quantum pseudocode, Los Alamos Technical Report LA-UR-96-2724 (1996), https://doi.org/10.2172/366453

  178. Kochen, S.: Ultraproducts in the theory of models. Ann. Math. 74(2), 221–261 (1961). https://doi.org/10.2307/1970235

    Article  MathSciNet  Google Scholar 

  179. Kohno, T.: Conformal field theory and topology, Transl Math. Monogr. 210, Amer. Math. Soc., Providence, RI (2002), [ams:mmono-210]

  180. Kohno, T.: Homological representations of braid groups and KZ connections. J. Singularities 5, 94–108 (2012). https://doi.org/10.5427/jsing.2012.5g

    Article  MathSciNet  Google Scholar 

  181. Kolganov, N., Mironov, S., Morozov, A.: Large \(k\) topological quantum computer. Nucl. Phys. B 987, 116072 (2023). https://doi.org/10.1016/j.nuclphysb.2023.116072. [ar**v:2105.03980]

    Article  MathSciNet  Google Scholar 

  182. Kolmogorov, A.: Zur Deutung der intuitionistischen Logik. Math. Z. 35, 58–65 (1932). https://doi.org/10.1007/BF01186549

    Article  MathSciNet  Google Scholar 

  183. Kraus, N.: The General Universal Property of the Propositional Truncation. In: TYPES 2014, Leibniz International Proceedings in Informatics (LIPIcs) 39 (2015) [ar**v:1411.2682] https://doi.org/10.4230/LIPIcs.TYPES.2014.111

  184. Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Logical Methods Comput. Sci. 9(1), 958 (2013). https://doi.org/10.2168/LMCS-9(1:1)2013. [ar**v:1106.3448]

    Article  MathSciNet  Google Scholar 

  185. Krömer, R.: Tool and Object: A History and Philosophy of Category Theory. Springer, Berlin (2007)

    Book  Google Scholar 

  186. Ladyman, J., Presnell, S.: Identity in homotopy type theory, part I: the justification of path induction. Philos. Math. 23(3), 386–406 (2015). https://doi.org/10.1093/philmat/nkv014

    Article  MathSciNet  Google Scholar 

  187. Lawvere, W.: Quantifiers and sheaves, Actes Congrès intern. Math. 1 (1970), 329-334, [ncatlab.org/nlab/files/Lawvere-QuantifiersAndSheaves.pdf]

  188. Lawvere, W.: Cohesive Toposes and Cantor’s “lauter Einsen.’’. Philos. Math. 2(1), 5–15 (1994). https://doi.org/10.1093/philmat/2.1.5

    Article  MathSciNet  Google Scholar 

  189. Lawvere, W.: Axiomatic cohesion. Theory 19(3), 41–49 (2007)

    MathSciNet  Google Scholar 

  190. Lee, E.-K.: A positive presentation of the pure braid group, J. Chungcheong Math. Soc. 23(3), 555-561, (2010), [JAKO201007648745187]

  191. van Leeuwen, J.: Wiedermann: Knowledge, Representation and the Dynamics of Computation, Studies in Applied Philosophy, vol. 28, pp. 69–89. Springer, Berlin (2017). https://doi.org/10.1007/978-3-319-43784-2_5

  192. Leinaas, J.M., Myrheim, J.: On the theory of identical particles. Nuovo Cim B 37, 1–23 (1977). https://doi.org/10.1007/BF02727953

    Article  ADS  Google Scholar 

  193. Lerda, A.: Anyons – Quantum Mechanics of Particles with Fractional Statistics, Lect. Notes Phys. 14, Springer, Berlin (1992), https://doi.org/10.1007/978-3-540-47466-1

  194. Lewis, C.I.: A Survey of Symbolic Logic, Univ. of California Press, Berkeley, (1918), [archive.org/details/surveyofsymbolic00lewiiala]

  195. Leymann, F., Barzen, J.: The bitter truth about gate-based quantum algorithms in the NISQ era. Quant. Sci. Technol. 5, 044007 (2020). https://doi.org/10.1088/2058-9565/abae7d

    Article  ADS  Google Scholar 

  196. Li, N.: Quotient Types in Type Theory, PhD Thesis, Nottingham (2014), [eprints.nottingham.ac.uk:28941], [ncatlab.org/nlab/files/Li-QuotientTypes.pdf]

  197. Liao, A., Coates, J., Mullanix, R.: 1lab, [https://1lab.dev]

  198. Licata, D., Finster, E.: Eilenberg-MacLane spaces in homotopy type theory, CSL-LICS ‘14 66, 1-9, (2014) https://doi.org/10.1145/2603088.2603153

  199. Lubarsky, R.: On the cauchy completeness of the constructive cauchy reals. Electron. Notes Theor. Comput. Sci. 167, 225–254 (2007). https://doi.org/10.1016/j.entcs.2006.09.012

    Article  MathSciNet  Google Scholar 

  200. Lüders, G.: Über die Zustandsänderung durch den Meßprozeß. Ann. Phys. 8, 322–328 (1951)

    Google Scholar 

  201. Lundfall, M.: Formalizing real numbers in Agda, preprint (2015), [ncatlab.org/nlab/files/Lundfall-RealNumbersInAgda.pdf]

  202. Luo, Z.: Computation and Reasoning–A Type Theory for Computer Science, Clarendon Press, Oxford (1994), [ISBN:9780198538356]

  203. Lurie, J.: Higher Topos Theory, Ann. Math. Stud. 170, Princeton University Press (2009), [pup:8957], [ar**v:math/0608040]

  204. Lurie, J.: Higher Algebra, [https://www.math.ias.edu/\(\sim \)lurie/papers/HA.pdf]

  205. Macaluso, E., Comparin, T., Mazza, L., Carusotto, I.: Fusion channels of non-abelian anyons from angular-momentum and density-profile measurements. Phys. Rev. Lett. 123, 266801 (2019). https://doi.org/10.1103/PhysRevLett.123.266801. [ar**v:1903.03011]

    Article  ADS  Google Scholar 

  206. Magnus, W., Karras, A., Solitar, D.: Combinatorial group theory: presentation of groups in terms of generators and relations, Dover Publications (2004), [ISBN-13:9780486438306]

  207. Manin, Y.I.: Algebraic curves over fields with differentiation (Russian), Izv. Akad. Nauk SSSR. Ser. Mast. 22 (1958), 737–756, [bookstore.ams.org/trans2-37], [books.google.com/books?id=fZ7ms3db_cMC]

  208. Manin, Y.I.: Computable and Uncomputable, Sov. Radio (1980), published in: Mathematics as Metaphor: Selected essays of Yuri I. Manin, Collected Works 20, AMS (2007), 69–77, [ISBN:978-0-8218-4331-4]

  209. Manin, Y.I.: Classical computing, quantum computing, and Shor’s factoring algorithm, Séminaire Bourbaki exp. 862, Astérisque 266 (2000), 375–404

  210. Marra, P.: Majorana nanowires for topological quantum computation: a tutorial. J. Appl. Phys. 132, 231101 (2022). https://doi.org/10.1063/5.0102999. [ar**v:2206.14828]

    Article  ADS  Google Scholar 

  211. Martin-Löf, P.: A Theory of Types, unpublished note (1971), [ncatlab.org/nlab/files/MartinLoef1971-ATheoryOfTypes.pdf]

  212. Martin-Löf, P.: An intuitionistic theory of types: predicative part. In: Logic Colloquium ‘73, Studies in Logic and the Foundations of Mathematics 80, 73–118, (1975)

  213. Martin-Löf, P.: Constructive mathematics and computer programming. Stud. Logic Found. Math. 104, 153–175 (1982). https://doi.org/10.1016/S0049-237X(09)70189-2

    Article  MathSciNet  Google Scholar 

  214. Martin-Löf, P.: (notes by G. Sambin of a series of lectures given in Padua in 1980), Intuitionistic type theory, Bibliopolis, Naples (1984), [ncatlab.org/nlab/files/MartinLofIntuitionisticTypeTheory.pdf]

  215. Martin-Löf, P.: On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Nordic J. Philosophical Logic 1 (1996), 11-60, [docenti.lett.unisi.it/files/4/1/1/6/martinlof4.pdf]

  216. Masaki, Y., Mizushima, T., Nitta, M.: Non-Abelian Anyons and Non-Abelian Vortices in Topological Superconductors, [ar**v:2301.11614]

  217. Mashayekhy, B., Mirebrahimi, H.: Some Properties of Finitely Presented Groups with Topological Viewpoints, Int. J. Math., Game Theory, and Algebra 18(6), 511-515, (2010), [ar**v:1012.1744]

  218. Matekole, E.S., Fang, Y.-L L., Lin, M.: Methods and Results for Quantum Optimal Pulse Control on Superconducting Qubit Systems, 2022 IEEE International Parallel and Distributed Processing Symposium Workshops (2022), https://doi.org/10.1109/IPDPSW55747.2022.00102, [ar**v:2202.03260]

  219. Mawson, T., Petersen, T., Slingerland, J., Simula, T.: Braiding and fusion of non-Abelian vortex anyons. Phys. Rev. Lett. 123, 140404 (2019). https://doi.org/10.1103/PhysRevLett.123.140404. [ar**v:1805.10009]

    Article  ADS  Google Scholar 

  220. May, P.: The Geometry of Iterated Loop Spaces. Springer, Berlin (1972). https://doi.org/10.1007/BFb0067491

  221. May, P.: Infinite loop space theory. Bull. Am. Math. Soc. 83(4), 456–494 (1977)

    Article  MathSciNet  Google Scholar 

  222. May, P., Sigurdsson, J.: Parametrized Homotopy Theory, Math. Surv. Monogr. 132 Amer. Math. Soc. (2006), [ISBN:9781470413590], [ar**v:math/0411656]

  223. Miller, W.: Symmetry Groups and Their Applications, Pure and Applied Mathematics 50, pp. 16–60, Elsevier, (1972) [ISBN:9780080873657]

  224. Miller, H. (ed.): Handbook of Homotopy Theory, Chapman and Hall/CRC Press (2019), [ISBN:9780815369707], https://doi.org/10.1201/9781351251624

  225. Milne, J.: Étale Cohomology, Mathematical Series 33, Princeton University Press (1980), [ISBN:9780691082387], [jstor:j.ctt1bpmbk1]

  226. Mochon, C.: Anyons from non-solvable finite groups are sufficient for universal quantum computation. Phys. Rev. A 67, 022315 (2003). https://doi.org/10.1103/PhysRevA.67.022315. [ar**v:quant-ph/0206128]

    Article  ADS  Google Scholar 

  227. Mochon, C.: Anyon computers with smaller groups. Phys. Rev. A 69, 032306 (2004). https://doi.org/10.1103/PhysRevA.69.032306. [ar**v:quant-ph/0306063]

    Article  ADS  Google Scholar 

  228. Møller, J.: The fundamental group and covering spaces, lecture notes, [ar**v:1106.5650]

  229. Munkres, J.: Topology, Pearson (2013), [ISBN:1292023627]

  230. Muro, F.: Representability of Cohomology Theories, talk at Joint Math. Conf, CSASC, Prague (2010), [ncatlab.org/nlab/files/Muro-Representability.pdf]

  231. Murray, Z.: Constructive Analysis in the Agda Proof Assistant, [ar**v:2205.08354], [github.com/z-murray/honours-project-constructive-analysis-in-agda]

  232. Myers, D.J.: Modal Fracture of Higher Groups, Diff. Geom. Appl. (2024, in print) [ar**v:2106.15390]

  233. Myers, D.J.: Orbifolds as microlinear types in synthetic differential cohesive homotopy type theory, [ar**v:2205.15887]

  234. Myers, D.J., Riley, M.: Commuting cohesions, [ar**v:2301.13780]

  235. Nayak, C., Simon, S.H., Stern, A., Freedman, M., Das Sarma, S.: Non-abelian anyons and topological quantum computation. Rev. Mod. Phys. 80, 1083–1159 (2008). https://doi.org/10.1103/RevModPhys.80.1083. [ar**v:0707.1889]

    Article  ADS  MathSciNet  Google Scholar 

  236. Nenciu, G.: On the adiabatic theorem of quantum mechanics. J. Phys. A: Math. Gen. 13, L15 (1980). https://doi.org/10.1088/0305-4470/13/2/002

    Article  ADS  MathSciNet  Google Scholar 

  237. Nielsen, M.A., Chuang, I.L.: Quantum Computation and Quantum Information, Cambridge University Press, (2010), [ISBN:9780511976667]

  238. Nielsen, M.A., Dowling, M.R., Gu, M., Doherty, A.C.: Quantum computation as geometry. Science 311(5764), 1133–1135 (2006). https://doi.org/10.1126/science.1121541. [ar**v:quant-ph/0603161]

    Article  ADS  MathSciNet  Google Scholar 

  239. Nikolaus, T., Schreiber, U., Stevenson, D.: Principal \(\infty \)-bundles - General theory. J. Homotopy Rel. Struc. 10, 749–801 (2015). https://doi.org/10.1007/s40062-014-0083-6. [ar**v:1207.0248]

    Article  MathSciNet  Google Scholar 

  240. Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990), [www.cse.chalmers.se/research/group/logic/book]

  241. Norell, U.: Dependently typed programming in Agda, in advanced functional programming AFP 2008. Lect. Notes Comput. Sci. 5832, 230–266 (2009). https://doi.org/10.1007/978-3-642-04652-0_5

    Article  ADS  Google Scholar 

  242. Ogburn, R.W., Preskill, J.: Topological Quantum Computation, In: Williams, C.P. (Ed.), Quantum Computing and Quantum Communications, Lect. Notes Comput. Sci. 1509, 341, Springer, Berlin (1999), https://doi.org/10.1007/3-540-49208-9-31

  243. Pachos, J.K.: Introduction to Topological Quantum Computation. Cambridge University Press, Cambridge (2012)

    Book  Google Scholar 

  244. Palmgren, E.: On Universes in Type Theory. In: Twenty-Five Years of Constructive Type Theory, Oxford University Press (1998), 191–204, https://doi.org/10.1093/oso/9780198501275.003.0012

  245. Paulin-Mohring, C.: Inductive definitions in the system Coq–Rules and Properties. In: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993), https://doi.org/10.1007/BFb0037116

  246. Pavlović, D.: Categorical interpolation: Descent and the Beck-Chevalley condition without direct images, In: Category Theory, Lecture Notes in Mathematics 1488, Springer, Berlin (1991), https://doi.org/10.1007/BFb0084229, [isg.rhul.ac.uk/dusko/papers/1990-BCDE-Como.pdf]

  247. Polyakov, A.: String theory and quark confinement. Nucl. Phys. Proc. Suppl. 68, 1–8 (1998). https://doi.org/10.1016/S0920-5632(98)00135-2. [ar**v:hep-th/9711002]

    Article  ADS  MathSciNet  Google Scholar 

  248. Polyakov, A.: The wall of the cave. Int. J. Mod. Phys. A 14, 645–658 (1999). https://doi.org/10.1142/S0217751X99000324. ar**v:hep-th/9809057

    Article  ADS  MathSciNet  Google Scholar 

  249. Polyakov, A.: Gauge Fields and Space-Time, Int. J. Mod. Phys. A 17 S1 (2002), 119–136, https://doi.org/10.1142/S0217751X02013071. [ar**v:hep-th/0110196],

  250. Potts, P., Edalat, A.: Exact real computer arithmetic, preprint (1997), [ncatlab.org/nlab/files/PottsEdalat-ExactRealComputerArithmetic.pdf]

  251. Preskill, J.: Quantum computing in the NISQ era and beyond. Quantum 2, 79 (2018)

    Article  Google Scholar 

  252. Preskill, J.: The Physics of Quantum Information, talk at The Physics of Quantum Information, 28th Solvay Conference on Physics (2022), [ar**v:2208.08064]

  253. Quillen, D.: Homotopical Algebra, Lecture Notes in Mathematics 43 Springer, (1967), https://doi.org/10.1007/BFb0097438

  254. Rajak, A., Suzuki, S., Dutta, A., Chakrabarti, B.K.: Quantum annealing: an overview. Phil. Trans. R. Soc. A 381, 20210417 (2022). https://doi.org/10.1098/rsta.2021.0417. [ar**v:2207.01827]

    Article  ADS  Google Scholar 

  255. Rao, S.: Introduction to abelian and non-abelian anyons, In: Topology and Condensed Matter Phys. Texts & Read. 19 Springer (2017), 399–437, https://doi.org/10.1007/978-981-10-6841-6_16, [ar**v:1610.09260]

  256. Renes, J.M.: Quantum Information Theory. De Gruyter, Basel (2022)

    Book  Google Scholar 

  257. Rezk, C.: Toposes and homotopy toposes, lecture notes (2010), [ncatlab.org/nlab/files/Rezk_HomotopyToposes.pdf]

  258. Rho, M., Zahed, I. (eds.): The Multifaceted Skyrmion, World Scientific, Singapore (2016), https://doi.org/10.1142/9710

  259. Richter, B.: From Categories to Homotopy Theory. Cambridge Studies in Advanced Mathematics, vol. 188. Cambridge University Press, Cambridge (2020)

    Book  Google Scholar 

  260. Rieffel, E., Polak, W.: Quantum Computing-A Gentle Introduction. MIT Press, Boston (2011)

    Google Scholar 

  261. Riehl, E.: Categorical Homotopy Theory, Cambridge University Press (2014), [ISBN:9781107048454]

  262. Riehl, E.: On the \(\infty \)-topos semantics of homotopy type theory, lecture at Logic and higher structures, CIRM (2022), [emilyriehl.github.io/files/semantics.pdf]

  263. Rigolin, G., Ortiz, G.: The adiabatic theorem for quantum systems with spectral degeneracy. Phys. Rev. A 85, 062111 (2012). https://doi.org/10.1103/PhysRevA.85.062111. [ar**v:1111.5333]

    Article  ADS  Google Scholar 

  264. Rijke, E.: Introduction to Homotopy Type Theory, lecture at CMU (2018) [www.andrew.cmu.edu/user/erijke/hott] [ncatlab.org/nlab/files/Rijke-IntroductionHoTT-2018.pdf]

  265. Rijke, E.: Classifying Types, PhD Thesis, Carnegie Mellon University, [ar**v:1906.09435]

  266. Rijke, E.: Introduction to Homotopy Type Theory, Cambridge University Press (in print), [ar**v:2212.11082]

  267. Rijke, E., Shulman, M., Spitters, B.: Modalities in Homotopy Type Theory, 16 (2020) 1, https://doi.org/10.23638/LMCS-16(1:2)2020, [ar**v:1706.07526]

  268. Rijke, E., Spitters, B.: Sets in homotopy type theory. Math. Struct. Comput. Sci. 25(5), 1172–1202 (2015). https://doi.org/10.1017/S0960129514000553. [ar**v:1305.3835]

    Article  MathSciNet  Google Scholar 

  269. Riley, M.: A Bunched Homotopy Type Theory for Synthetic Stable Homotopy Theory, PhD Thesis, Wesleyan University, (2022), https://doi.org/10.14418/wes01.3.139

  270. Ringer, T., Porter, R., Yazdani, N., Leo, J., Grossman, D.: Proof Repair across Type Equivalences, [ar**v:2010.00774]

  271. Roberts, C.D.: Origin of the Proton Mass, [ar**v:2211.09905]

  272. Roberts, C.D.: On Mass and Matter. AAPPS Bull. 31, 6 (2021). https://doi.org/10.1007/s43673-021-00005-4. [ar**v:2101.08340]

    Article  Google Scholar 

  273. Roberts, C.D., Schmidt, S.M.: Reflections upon the emergence of hadronic mass. Eur. Phys. J. Special Top. 229, 3319–3340 (2020). https://doi.org/10.1140/epjst/e2020-000064-6. [ar**v:2006.08782]

    Article  ADS  Google Scholar 

  274. Rotman, J.J.: An Introduction to the Theory of Groups. Springer, Berlin (1995)

    Book  Google Scholar 

  275. Rotman, J.J.: An Introduction to Algebraic Topology. Graduate Texts in Mathematics, vol. 119. Springer, Berlin (1988)

    Book  Google Scholar 

  276. Rowell, E.: Braids, Motions and Topological Quantum Computing, [ar**v:2208.11762]

  277. Rowell, E.C., Wang, Z.: Mathematics of Topological Quantum Computing. Bull. Am. Math. Soc. 55, 183–238 (2018). https://doi.org/10.1090/bull/1605. [ar**v:1705.06206]

    Article  MathSciNet  Google Scholar 

  278. Rudin, W.: Principles of Mathematical Analysis, McGraw-Hill (1976), [ISBN13:9780070542358]

  279. Rudolph, G., Schmidt, M.: Differential Geometry and Mathematical Physics – Part II. Fibre Bundles, Topology and Gauge Fields, Springer, Berlin (2017), https://doi.org/10.1007/978-94-024-0959-8

  280. Russell, B., Whitehead, A.: Principia Mathematica, Cambridge University Press (1910, 1927), [ISBN:9780521067911]

  281. Sakaguchi, K.: Validating Mathematical Structures, in: Automated Reasoning. IJCAR 2020, Lecture Notes in Computer Science 12167 Springer (2020), https://doi.org/10.1007/978-3-030-51054-1_8

  282. Santini, A.: Topological groupoids, Kandidatproject, Copenhagen University (2011), [ncatlab.org/nlab/files/Santini-Groupoids.pdf]

  283. Sati, H.: M-theory and matter via twisted equivariant differential (TED) K-theory, talk at M-Theory and Mathematics 2023, CQTS @ NYU Abu Dhabi (2023)

  284. Sati, H., Schreiber, U.: Differential Cohomotopy implies intersecting brane observables via configuration spaces and chord diagrams, Adv. Theor. Math. Physics 26 (2022) 4, [ISSN:1095-0753], [ar**v:1912.10425]

  285. Sati, H., Schreiber, U.: Equivariant Cohomotopy implies orientifold tadpole cancellation. J. Geom. Phys. 156, 103775 (2020). https://doi.org/10.1016/j.geomphys.2020.103775. [ar**v:1909.12277]

    Article  MathSciNet  Google Scholar 

  286. Sati, H., Schreiber, U.: Proper Orbifold Cohomology, [ar**v:2008.01101]

  287. Sati, H., Schreiber, U.: M/F-Theory as \(M\!f\)-Theory, Rev. Math. Phys. 35 10 (2023) [ar**v:2103.01877] https://doi.org/10.1142/S0129055X23500289

  288. Sati, H., Schreiber, U.: Equivariant principal \(\infty \)-bundles, [ar**v:2112.13654]

  289. Sati, H., Schreiber, U.: Anyonic defect branes in TED-K-theory. Rev. Math. Phys. (2023). https://doi.org/10.1142/S0129055X23500095. [ar**v:2203.11838]

    Article  Google Scholar 

  290. Sati, H., Schreiber, U.: Anyonic topological order in TED-K-theory. Rev. Math. Phys. 35(03), 2350001 (2023). https://doi.org/10.1142/S0129055X23500010. [ar**v:2206.13563]

    Article  Google Scholar 

  291. Sati, H., Schreiber, U.: Topological Quantum Programming in TED-K, PlanQC 2022 33 (2022), [ar**v:2209.08331], [ncatlab.org/schreiber/show/Topological+Quantum+Programming+in+TED-K]

  292. Sati, H., Schreiber, U.: Entanglement of Sections: The pushout of entangled and parameterized quantum information [ar**v:2309.07245]

  293. Sati, H., Schreiber, U.: The Quantum Monadology, [ar**v:2310.15735]

  294. Sati, H., Schreiber, U., Stasheff, J.: Twisted differential string and fivebrane structures. Commun. Math. Phys. 315, 169–213 (2012). https://doi.org/10.1007/s00220-012-1510-3. [ar**v:0910.4001]

    Article  ADS  MathSciNet  Google Scholar 

  295. Sau, J.: A Roadmap for a Scalable Topological Quantum Computer, Physics 10 (2017) 68, [physics.aps.org/articles/v10/68]

  296. Schreiber, U.: Differential cohomology in a cohesive \(\infty \)-topos, Habilitation thesis, [ar**v:1310.7930]

  297. Schreiber, U.: Quantization via Linear Homotopy Types, talk notes, Paris Diderot and ESI Vienna (2014), [ar**v:1402.7041]

  298. Schreiber, U.: Differential generalized cohomology in Cohesive homotopy type theory, talk at Formalization of Mathematics, Inst. H. Poincaré, Paris (May 2014), [ncatlab.org/schreiber/files/SchreiberParis2014.pdf]

  299. Schreiber, U.: Some thoughts on the future of modal homotopy type theory, talk at German Mathematical Society meeting, Hamburg (Sept 2015), [ncatlab.org/schreiber/files/SchreiberDMV2015b.pdf]

  300. Schreiber, U.: Knots for quantum computation from defect branes, talk at Workshop on Topological Methods in Mathematical Physics, Erice (Sep 2022), [ncatlab.org/schreiber/show/Knots+for+quantum+computation+from+defect+branes]

  301. Schreiber, U.: Quantum types via Linear Homotopy Type Theory, talk at Workshop on Quantum Software @ QTML2022, Naples (Nov 2022), [ncatlab.org/schreiber/files/QuantumDataInLHoTT-221117.pdf]

  302. Schreiber, U.: Topological Quantum Gates from M-Theory, talk at M-Theory and Mathematics 2023, CQTS @ NYU Abu Dhabi (2023)

  303. Schreiber, U., Shulman, M.: Quantum Gauge field theory in cohesive homotopy type theory. EPTCS 158, 109–126 (2014). https://doi.org/10.4204/EPTCS.158.8. [ar**v:1408.0054]

    Article  Google Scholar 

  304. Schubert, H.: Categories. Springer, Berlin (1972)

    Book  Google Scholar 

  305. Schwarz, J.: The Second Superstring Revolution, lecture at Sakharov Conference (Moscow, May 1996), [inspire:969846], [ar**v:hep-th/9607067]

  306. Scott, D.S.: Outline of a mathematical theory of computation, in: Proc. 4th Ann. Princeton Conf. on Information Sciences and Systems (1970), 169-176, [ncatlab.org/nlab/files/Scott-TheoryOfComputation.pdf]

  307. Scott, D.S., Strachey, C.: Toward a Mathematical Semantics for Computer Languages, Oxford Univ. Computing Laboratory, Technical Monograph PRG-6 (1971), [www.cs.ox.ac.uk/files/3228/PRG06.pdf]

  308. Seely, R.A.G.: Locally cartesian closed categories and type theory. Math. Proc. Camb. Phil. Soc. 95, 33–48 (1984). https://doi.org/10.1017/S0305004100061284

    Article  MathSciNet  Google Scholar 

  309. Segal, G.: Configuration-spaces and iterated loop-spaces. Invent. Math. 21, 213–221 (1973). https://doi.org/10.1007/BF01390197

    Article  ADS  MathSciNet  Google Scholar 

  310. Selinger, P.: Towards a quantum programming language. Math. Struct. Comput. Sci. 14, 527–586 (2004). https://doi.org/10.1017/S0960129504004256

    Article  MathSciNet  Google Scholar 

  311. Shor, P.W.: Algorithms for quantum computation: discrete logarithms and factoring. In: Proceedings of 35th Annual Symposium on Foundations of Computer Science (1994), pp. 124–134, https://doi.org/10.1109/SFCS.1994.365700

  312. Shor, P.W.: Scheme for reducing decoherence in quantum computer memory. Phys. Rev. A 52, R2493(R) (1995). https://doi.org/10.1103/PhysRevA.52.R2493

    Article  ADS  Google Scholar 

  313. Shulman, M.: Minicourse on Homotopy Type Theory, University of Swansea (2012), [http://home.sandiego.edu/\(\sim \)shulman/hottminicourse2012]

  314. Shulman, M.: Univalence for inverse diagrams and homotopy canonicity. Math. Struct. Comput. Sci. 25(5), 1203–1277 (2015). https://doi.org/10.1017/S0960129514000565. [ar**v:1203.3253]

    Article  MathSciNet  Google Scholar 

  315. Shulman, M.: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory. Math. Struct. Comput. Sci. 28(6), 856–941 (2018). https://doi.org/10.1017/S0960129517000147. [ar**v:1509.07584]

    Article  MathSciNet  Google Scholar 

  316. Shulman, M.: All \((\infty ,1)\)-toposes have strict univalent universes, [ar**v:1904.07004]

  317. Simon, B.: Holonomy, the quantum adiabatic theorem, and Berry’s phase. Phys. Rev. Lett. 51, 2167–2170 (1983). https://doi.org/10.1103/PhysRevLett.51.2167

    Article  ADS  MathSciNet  Google Scholar 

  318. Simon, D.R.: On the power of quantum computation. SIAM J. Comput. 26, 5 (1997). https://doi.org/10.1137/S0097539796298637

    Article  MathSciNet  Google Scholar 

  319. Simon, S.H.: Topological Quantum, lecture notes and proto-book (2021), [www-thphys.physics.ox.ac.uk/people/SteveSimon/topological2021/TopoBook-Sep1-2021.pdf]

  320. Simpson, C.: A Giraud-type characterization of the simplicial categories associated to closed model categories as \(\infty \)-pretopoi, [ar**v:math/9903167]

  321. Slonneger, K., Kurtz, B.: Denotational semantics, Formal Syntax and Semantics of Programming Languages, Addison-Wesley (1995), [https://homepage.divms.uiowa.edu/~ slonnegr/plf/Book/]

  322. Solovay, R.: Lie Groups and Quantum Circuits, talk in: Mathematics Of Quantum Computation workshop, MSRI (2000), [msri.org/workshops/189/schedules/12826]

  323. Sorensen, M.H., Urzyczyn, P.: Lectures on the Curry-Howard isomorphism, Studies in Logic 149, Elsevier (2006), [ISBN:9780444520777]

  324. Spanier, E.: Algebraic Topology. Springer, Berlin (1982)

    Google Scholar 

  325. Stanescu, T.D.: Introduction to Topological Quantum Matter & Quantum Computation, CRC Press (2020), [ISBN:9780367574116]

  326. Steenrod, N.: Homology With Local Coefficients, Ann. Math. Sec. Ser. 44 (1943), 610-627, [jstor:1969099]

  327. Stern, A., Lindner, N.H.: Topological quantum computation-from basic concepts to first experiments. Science 339(6124), 1179–1184 (2013). https://doi.org/10.1126/science.1231473

    Article  ADS  Google Scholar 

  328. Streicher, T.: Investigations into Intensional Type Theory, Habilitation Thesis, Darmstadt (1993), [ncatlab.org/nlab/files/Streicher-IntensionalTT.pdf]

  329. Strocchi, F.: An Introduction to Non-Perturbative Foundations of Quantum Field Theory. Oxford University Press, Oxford (2013)

    Book  Google Scholar 

  330. Strom, J.: Modern Classical Homotopy Theory, Graduate Studies in Mathematics 127, Amer. Math. Soc., Providence, RI (2011), https://doi.org/10.1090/gsm/127

  331. Stump, A.: Verified Functional Programming in Agda. Association for Computing Machinery and Morgan & Claypool (2016). https://doi.org/10.1145/2841316

  332. Thompson, S.: Type Theory and Functional Programming, Addison-Wesley (1991), [ISBN:0201416670]

  333. Todorov, I., Hadjiivanov, L.: Monodromy Representations of the Braid Group. Phys. Atom. Nucl. 64, 2059–2068 (2001). https://doi.org/10.1134/1.1432899. [ar**v:hep-th/0012099]

    Article  ADS  MathSciNet  Google Scholar 

  334. Toën, B., Vezzosi, G.: Homotopical algebraic geometry I: Topos theory. Adv. Math. 193(2), 257–372 (2005). https://doi.org/10.1016/j.aim.2004.05.004. [ar**v:math/0207028]

    Article  MathSciNet  Google Scholar 

  335. tom Dieck, T.: Transformation Groups, de Gruyter (1987), https://doi.org/10.1515/9783110858372

  336. tom Dieck, T.: Algebraic topology, Eur. Math. Soc. (2008), https://doi.org/10.4171/048

  337. Troelstra, A.S.: Principles of Intuitionism. Lecture Notes in Mathematics, vol. 95. Springer, Berlin (1969)

  338. Troelstra, A.S.: Aspects of constructive mathematics. Stud. Logic Found. Math. 90, 973–1052 (1977). https://doi.org/10.1016/S0049-237X(08)71127-3

    Article  MathSciNet  Google Scholar 

  339. Troelstra, A.S., van Dalen, D.: Constructivism in Mathematics – An introduction, Vol 1, Studies in Logic and the Foundations of Mathematics 121, North Holland (1988), [ISBN:9780444702661]

  340. Tsementzis, D.: Univalent foundations as structuralist foundations. Synthese 194(9), 3583–3617 (2017). https://doi.org/10.1007/s11229-016-1109-x

    Article  MathSciNet  Google Scholar 

  341. UniMath, [unimath.github.io/UniMath], [unimath.github.io/agda-unimath]

  342. Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics, Institute for Advanced Study, Princeton, 2013, [homotopytypetheory.org/book]

  343. Valera, S.J.: Fusion structure from exchange symmetry in \((2+1)\)-Dimensions. Ann. Phys. 429, 168471 (2021). https://doi.org/10.1016/j.aop.2021.168471. [ar**v:2004.06282]

    Article  MathSciNet  Google Scholar 

  344. van den Berg, B., Garner, R.: Types are weak \(\omega \)-groupoids. Proc. London Math. Soc. 102(2), 370–394 (2011). https://doi.org/10.1112/plms/pdq026. [ar**v:0812.0298]

    Article  MathSciNet  Google Scholar 

  345. Vanderbilt, D.: Berry Phases in Electronic Structure Theory-Electric Polarization. Orbital Magnetization and Topological Insulators. Cambridge University Press, Cambridge (2018)

    Book  Google Scholar 

  346. van Doorn, F.: On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory, PhD dissertation, Carnegie Mellon (2018), [ar**v:1808.10690]

  347. Veltri, N., van der Weide, N.: Constructing Higher Inductive Types as Groupoid Quotients, Logical Methods in Computer Science 17 2 (2021), https://doi.org/10.23638/LMCS-17(2:8)2021, [ar**v:2002.08150]

  348. Vezzosi, A., Mörtberg, A., Abel, A.: Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types. In: Proceedings of the ACM on Programming Languages 3 ICFP 87 (2019), 1-29, https://doi.org/10.1145/3341691

  349. Voevodsky, V.: Univalent Foundations Project, grant proposal application (2010), [ncatlab.org/nlab/files/Voevodsky-UFP2010.pdf]

  350. Voisin, C.: Hodge theory and Complex algebraic geometry I, translated by L. Schneps, Cambridge University Press (2002/3), https://doi.org/10.1017/CBO9780511615344

  351. Voisin, C.: Hodge theory and Complex algebraic geometry II, translated by L. Schneps, Cambridge University Press (2002/3), https://doi.org/10.1017/CBO9780511615177

  352. von Neumann, J.: Mathematische Grundlagen der Quantenmechanik, Springer (1932, 1971), https://doi.org/10.1007/978-3-642-96048-2; translated as: Mathematical Foundations of Quantum Mechanics Princeton University Press (1955), https://doi.org/10.1515/9781400889921

  353. Vuillemin, J.: Exact real computer arithmetic with continued fractions, in LFP ‘88: Proceedings of the 1988 ACM conference on LISP and functional programming (1988), pp. 14-27, https://doi.org/10.1145/62678.62681

  354. Wadler, P.: Propositions as types. ACM Commun. 58(12), 75–84 (2015). https://doi.org/10.1145/2699407

    Article  Google Scholar 

  355. Wang, Z.: Topological Quantum Computation, CBMS Regional Conference Series in Mathematics 112 Amer. Math. Soc. (2010), [ISBN-13:978082184930-9]

  356. Wärn, D.: Eilenberg-MacLane spaces and stabilisation in homotopy type theory, [ar**v:2301.03685]

  357. Weinstein, A.: Groupoids: Unifying Internal and External Symmetry – A Tour through some Examples, Notices Amer. Math. Soc. 43 (1996), 744-752, [www.ams.org/notices/199607/weinstein.pdf]

  358. Wellen, F.: Cartan Geometry in Modal Homotopy Type Theory, PhD Thesis, KIT (2017), [ar**v:1806.05966], [ncatlab.org/schreiber/show/thesis+Wellen]

  359. Wen, X.-G.: Topological orders and Chern-Simons theory in strongly correlated quantum liquid. Int. J. Mod. Phys. B 05(10), 1641–1648 (1991). https://doi.org/10.1142/S0217979291001541

    Article  ADS  MathSciNet  Google Scholar 

  360. Wilczek, F., Zee, A.: Appearance of gauge structure in simple dynamical systems. Phys. Rev. Lett. 52(24), 2111–2114 (1984). https://doi.org/10.1103/PhysRevLett.52.2111

    Article  ADS  MathSciNet  Google Scholar 

  361. Williams, L.: Configuration Spaces for the Working Undergraduate, Rose-Hulman Undergrad. Math. J. 21 (2020) 8, [rhumj:vol21/iss1/8], [ar**v:1911.11186]

  362. Wilson, J.C.H.: The geometry and topology of braid groups, lecture at 2018 Summer School on Geometry and Topology, Chicago (2018), [ncatlab.org/nlab/files/Wilson-BraidGroups.pdf]

  363. Yang, C.N., Ge, M.L. (eds.), Braid Group, Knot Theory and Statistical Mechanics, Adv. Ser. Mat. Phys. 9, World Scientific, Singapore (1991), https://doi.org/10.1142/0796

  364. Yap, C.-K., Dubé, T.: The exact computation paradigm. In: Computing in Euclidean Geometry, Lecture Notes Series on Computing, World Scientific (1995), 452-492, https://doi.org/10.1142/9789812831699_0011

  365. Zaanen, J., Liu, Y., Sun, Y.-W., Schalm, K.: Holographic Duality in Condensed Matter Physics. Cambridge University Press, Cambridge (2015)

    Book  Google Scholar 

  366. Zanardi, P., Rasetti, M.: Holonomic quantum computation. Phys. Lett. A 264, 94–99 (1999). https://doi.org/10.1016/S0375-9601(99)00803-8. [ar**v:quant-ph/9904011]

    Article  ADS  MathSciNet  Google Scholar 

  367. Zucker, J.: Formalization of Classical Mathematics in Automath, Colloq. Internat. Cent. Nat. Rech. Scient. 249 (1975), 135-145, [www.win.tue.nl/automath/archive/webversion/aut042/aut042.html]; also in: Studies in Logic and the Foundations of Mathematics 133 (1994), 127-139, https://doi.org/10.1016/S0049-237X(08)70202-7

  368. Zulehner, A., Wille, R.: Simulation and Design of Quantum Circuits, in: Reversible Computation: Extending Horizons of Computing. RC 2020, Lecture Notes in Computer Science 12070, Springer, New York (2020), https://doi.org/10.1007/978-3-030-47361-7_3

Download references

Author information

Authors and Affiliations

  1. Mathematics, Division of Science, Abu Dhabi, UAE

    David Jaz Myers, Hisham Sati & Urs Schreiber

  2. Center for Quantum and Topological Systems, NYUAD Research Institute, New York University, Abu Dhabi, UAE

    David Jaz Myers, Hisham Sati & Urs Schreiber

  3. The Courant Institute for Mathematical Sciences, New York, NYU, UAE

    Hisham Sati

Authors
  1. David Jaz Myers
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hisham Sati
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Urs Schreiber
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Urs Schreiber.

Additional information

Communicated by A. Childs.

In Memoriam of Yuri Manin who introduced quantum computation as well as Gauss-Manin connections unknowing of their close relationship.

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

The authors acknowledge the support by Tamkeen under the NYU Abu Dhabi Research Institute grant CG008..

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Myers, D.J., Sati, H. & Schreiber, U. Topological Quantum Gates in Homotopy Type Theory. Commun. Math. Phys. 405, 172 (2024). https://doi.org/10.1007/s00220-024-05020-8

Download citation

  • Received:

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s00220-024-05020-8

Search

Navigation