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 program equivalences. In particular, even the most simplistic univalent model enjoys many new equations that do not hold when the same constructions are carried out in the universes of traditional set-level (extensional) type theory.

翻译：我们在一版预见性保护同伦类型论中，为通用引用类型发展了外延语义，这是将合成保护域论应用于弗耶伍德斯基单一值基础理论的一种适配。我们首次观察到单一值对可变状态外延性语义的深远影响。单一值自动确保所有计算在堆对称性下保持不变——这是程序等价性丰富的来源。特别地，即使在最简单的单一值模型中，也享有许多当相同构造在传统集合级（外延）类型论的宇宙中执行时不成立的新等式。