发表机构
University of Gothenburg; Chalmers University of Technology（哥德堡大学; 查尔姆斯理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文在带擦除注解的类型论中，将擦除公设的保证扩展到同一类型，并利用擦除公设支持商类型，同时研究了擦除同一性证明的传递安全性，并附有Agda机器证明。
AI 中文摘要
本文关注如下问题：在带有擦除注解的类型论中，是否可以公设某些类型被占据，同时仍保证程序不会卡住。先前的工作已为一致的擦除公设（即被限制在擦除上下文中使用的公设）提供了此类保证。本文将保证扩展到带有同一类型的类型论。类似的想法为支持商类型提供了一种简单途径：本文表明，可以将诸如“两个相关值的等价类是相等的”这样的命题设为擦除公设，并拥有一个仅对等价类构造子计算的消去子，同时仍能保证程序正确计算。另一个问题是，如果允许使用擦除的同一性证明进行传递（转换），程序是否能正确计算。本文表明，在没有商类型和公设的情况下，以及存在商类型和可通过相等性反射实现的擦除公设时，这种操作是安全的。然而，此类无限制的传递与擦除的、公设的宇宙公理不兼容。为此，本文研究了函数[]-cong，它封装了擦除同一性证明的一种受限传递形式。本文附有机器检查的Agda证明。
英文摘要
This text is concerned with the question of whether, in type theory with erasure annotations, one can postulate that some type is inhabited and still have a guarantee that a program will not get stuck. Previous work has provided such guarantees for consistent erased postulates, i.e. postulates that are restricted to be used in erased contexts. Here those guarantees are extended to type theory with identity types. Similar ideas provide a simple way to support quotient types: it is shown that one can let things like "the equivalence classes for two related values are equal" be erased postulates and have an eliminator that only computes for the equivalence class constructor, and still get a guarantee that programs will compute correctly. Another question is whether programs compute correctly if one is allowed to transport (cast) using erased identity proofs. It is shown that this is safe in the absence of quotients and postulates, and in the presence of quotients and erased postulates that can be implemented using equality reflection. However, unrestricted transports of this kind are not compatible with erased, postulated univalence. For that reason the text includes a study of the function []-cong, which encapsulates a limited form of transport for erased identity proofs. The text is accompanied by machine-checked Agda proofs.
