解放自等价参考类型的自由定理
摘要：不同参考类型在受控同伦类型论的非预测版本中的指示性语义，这是对Voedvsky共价基础上的合成保守域论的一种适应。我们首次观察到共价对可变状态的指示性语义有深远影响。共价自动确保所有计算在堆的对称性下是不变的——这是一种丰富的免费定理的源泉。特别地，即使是最简单的共价模型也具有许多在传统集合水平（外延性）类型论的宇宙中进行相同构造时是不存在的新的程序等同性。
作者：Jonathan Sterling, Daniel Gratzer, Lars Birkedal
论文ID：2307.16608
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-08-01