Erasure enriches type theory with a distinction between runtime relevant and irrelevant data, allowing the compilation step to safely erase the latter. Versions of this feature are implemented by many systems, including Agda, Idris, and Rocq. We present a structural version of type theory with erasure, formulated as a second-order generalised algebraic theory (SOGAT). Erasure is encoded as a phase distinction between runtime and erased terms, in the form of a proposition that can appear in a context. This formulation has several advantages: it has models based on categories with families, is compatible with other structural features such as staging, and provides a better guideline for implementation. Through the model theory of SOGATs, we study the semantics of type theory with erasure in families of sets, which generalises to any Grothendieck topos equipped with a tiny proposition. We establish conservativity over Martin-Löf type theory (MLTT) in both phases. For code extraction, we construct a presheaf model that produces untyped lambda calculus programs and prove its correctness through gluing. Our results are formalised in Agda and we provide a toy elaborator implementation.

翻译：擦除为类型论增添了运行时相关数据与无关数据的区分，使编译阶段能够安全地删除后者。许多系统（包括Agda、Idris和Rocq）都实现了该功能的变体。我们提出了一种含擦除的结构化类型论，将其形式化为二阶广义代数理论（SOGAT）。擦除被编码为运行时项与擦除项之间的阶段区分，表现为可出现在语境中的命题形式。这种形式化具有多项优势：它拥有基于含族范畴的模型，与阶段性等其他结构化特性兼容，并为实现提供了更优的指导。通过SOGAT的模型论，我们在集合族中研究了含擦除类型论的语义，该语义可推广至任何配备微命题的格罗腾迪克拓扑。我们建立了两个阶段相对于马丁-勒夫类型论（MLTT）的保守性。对于代码提取，我们构造了一个产生无类型lambda演算程序的预层模型，并通过粘合证明了其正确性。我们的结果已在Agda中形式化，并提供了玩具级实现器。