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 \({\mathbb {Z}_{2}}\) -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 \(\infty \) -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).
