We develop a denotational semantics for general reference types in an impredicative version of guarded homotopy type theory, an adaptation of synthetic guarded domain theory to Voevodsky's univalent foundations. We observe for the first time the profound impact of univalence on the denotational semantics of mutable state. Univalence automatically ensures that all computations are invariant under symmetries of the heap -- a bountiful source of free theorems. In particular, even the most simplistic univalent model enjoys many new program equivalences that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.

翻译：我们在守卫同伦类型理论（一种将综合守卫域理论适应于Voevodsky单值基础的可谓词版本）中，为通用引用类型构建了指称语义。首次观察到单值性对可变状态指称语义的深远影响。单值性自动确保所有计算在堆的对称性下保持不变——这为自由定理提供了丰饶的源泉。特别地，即便在最简单的单值模型中，也能得到诸多在传统集合层次（外延）类型论宇宙中相同构造所不具备的新程序等价关系。