To ensure decidability and consistency of its type theory, a proof assistant should only accept terminating recursive functions and productive corecursive functions. Most proof assistants enforce this through syntactic conditions, which can be restrictive and non-modular. Sized types are a type-based alternative where (co)inductive types are annotated with additional size information. Well-founded induction on sizes can then be used to prove termination and productivity. An implementation of sized types exists in Agda, but it is currently inconsistent due to the addition of a largest size. We investigate an alternative approach, where intensional type theory is extended with a large type of sizes and parametric quantifiers over sizes. We show that inductive and coinductive types can be constructed in this theory, which improves on earlier work where this was only possible for the finitely-branching inductive types. The consistency of the theory is justified by an impredicative realisability model, which interprets the type of sizes as an uncountable ordinal.

翻译：为确保类型论的可判定性与一致性，证明辅助工具应仅接受终止的递归函数与产出的共递归函数。大多数证明辅助工具通过语法条件强制执行此要求，但这些条件往往具有限制性且缺乏模块化。尺寸类型是一种基于类型的替代方案，其中（共）归纳类型通过附加的尺寸信息进行标注。随后可利用尺寸上的良基归纳来证明终止性与产出性。尺寸类型已在Agda中实现，但由于引入了最大尺寸，当前存在不一致性问题。我们研究了一种替代方法，即在内涵类型论中扩展一个大型尺寸类型及尺寸上的参数化量词。我们证明在此理论中可构造归纳类型与共归纳类型，这改进了早期仅能对有限分支归纳类型实现此构造的工作。该理论的一致性通过一个非直谓可实现性模型得到验证，该模型将尺寸类型解释为一个不可数序数。