标题： 量子与现实 显示英文标题

标题： Quantum and Reality

摘要： 在范畴论和类型论中对量子信息理论的形式化，为了设计可验证的量子编程语言，需要表达其两个基本特征：(1) 参数化线性性和 (2) 度量性。第一个自然地由依赖-线性类型语言如 Proto-Quipper 解决，或者根据我们最近的观察：线性同伦类型论（LHoTT）。第二个点仅以“自伴范畴”的语义形式受到广泛关注，在这种语义中，算子伴随被公理化，但它们对厄米特伴随的指定仍需手动施加。我们描述了一种自然出现的厄米特性，它根植于等变同伦理论的原则，适用于同伦类型语言，并自然地与由扭曲等变 KR-理论分类的拓扑量子态相连。具体来说，我们观察到当复数被视为 Z/2 等变实线性类型中的单对象时，通过共轭复数，有限维希尔伯特空间确实成为内部复数实模中的自对偶对象。关键在于这种厄米形式的构造不需要环境线性类型理论的其他条件，只需张量单位类型的负单位项。我们观察到这样的项在 LHoTT 中是可以构造的，它解释为球面谱的无穷群单位中的一个元素，将量子理论的基础与同伦理论联系起来。最后，我们指出这如何允许在嵌入到 LHoTT 中的量子语言中对量子门和量子通道的幺正性进行编码（和验证）。 显示英文摘要

摘要： 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. The first is naturally addressed by dependent-linearly typed languages such as Proto-Quipper or, following our recent observations: Linear Homotopy Type Theory (LHoTT). The second point has received much 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. 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 KR-theory. Namely, we observe that when the complex numbers are considered as a monoid internal to Z/2-equivariant real linear types, via complex conjugation, then (finite-dimensional) Hilbert spaces do become self-dual objects among internally-complex Real modules. 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 LHoTT, where it interprets as an element of the infinity-group of units of the sphere spectrum, tying the foundations of quantum theory to homotopy theory. We close by indicating how this allows for encoding (and verifying) the unitarity of quantum gates and of quantum channels in quantum languages embedded into LHoTT.