Quantum and reality

2026-03-31

PRE

Schreiber, Urs

DOI：10.1007/s40509-026-00395-w

Original

Original request for help

Save

Abstract

En 中文

Formalizations of quantum information theory in category theory and type theory, for the design of verifiable quantum programming languages, need to express its two fundamental characteristics: (1) parameterized linearity and (2) metricity, namely Hermiticity. The first is naturally addressed by dependent-linearly typed languages such as Proto- Quipper or, following our recent observations (Sati and Schreiber in Quantum Stud: Math Found 12:25, 2025; Sati and Schreiber in Quantum Stud: Math Found 2026): Linear Homotopy Type Theory ( LHoTT ). The second point has received substantial attention (only) in the form of semantics in dagger-categories, where operator adjoints are axiomatized, but their specification to Hermitian adjoints still needs to be imposed by hand. In this brief note, we describe a natural emergence of Hermiticity which is rooted in principles of equivariant homotopy theory, lends itself to homotopically-typed languages, and naturally connects to topological quantum states classified by twisted equivariant Real K-theory (with capital R: KR-theory). Namely, we observe that when the complex numbers are considered as a monoid internal to Z2\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\mathbb {Z}_{2}}$$\end{document}-equivariant real linear types, via complex conjugation (the Real numbers, with capital R), then (finite-dimensional) Hilbert spaces do become self-dual objects among internally complex Real modules. This move absorbs the dagger-structure into the type structure; for instance, a complex linear map is unitary iff seen internally to Real modules it is orthogonal. The point is that this construction of Hermitian forms requires of the ambient linear type theory nothing further than a negative unit term of tensor unit type. We observe that just such a term is constructible in plain LHoTT , where it interprets as the non-trivial degree=0 element of the infinity\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\infty $$\end{document}-group of units of the sphere spectrum, interestingly tying the foundations of quantum theory to homotopy theory. We close by indicating how this observation allows for encoding (and verifying) the unitarity of quantum gates and of quantum channels in quantum languages embedded into LHoTT , as described in Sati and Schreiber (Quantum Stud: Math Found 12:25, 2025).

Keywords:

Quantum information theory

Hermitian forms

Linear type theory

Quantum programming languages

Quantum and reality

Abstract

Journal

Organization

Cited Papers

Citing Papers