Type theories with multi-clocked guarded recursion provide a flexible framework for programming with coinductive types encoding productivity in types. Combining this with solutions to general guarded domain equations one can also construct relatively simple denotational models of programming languages with advanced features. These constructions have previously been explored in the setting of extensional type theory through a presheaf model, which proves correctness of encodings of W-types. That model has been adapted to presheaves of cubical sets (functors into the category of cubical sets), where the model verifies correctness of encodings also of coinductive types whose definitions involve quotient inductive types such as finite powersets or finite distributions. Likewise the cubical model also verifies correctness of coinductive predicates defined using existential quantification and allows the results to be related to the global world of cubical sets. This paper looks at how to extend the extensional presheaf model of multi-clocked guarded recursion to higher ordinals, so that correctness of encodings of coinductive types can be extended from W-types to those involving finite powersets and finite distributions, as well as coinductive predicates involving existential quantification. This extension will allow results previously proved in Clocked Cubical Type Theory to be interpreted in a model based on set-theory, proving the correctness of these results as understood in their usual set theoretic interpretation.

翻译：具有多时钟守卫递归的类型理论为编码类型中生产力（productivity）的余归纳类型编程提供了灵活框架。将该框架与广义守卫域方程的解相结合，还可构建具有高级特性的编程语言的相对简单的指称模型。此前，这些构造已在外延类型理论的预层模型中得到探索，该模型证明了W类型编码的正确性。该模型已被适配至立方集（cubical sets）的预层（从索引范畴到立方集范畴的函子），在此模型中，对于涉及商归纳类型（如有限幂集或有限分布）的余归纳类型定义，编码的正确性同样得到验证。类似地，基于存在量化的余归纳谓词的正确性在立方模型中也得到验证，并可将结果关联至全局立方集范畴。本文探讨如何将多时钟守卫递归的外延预层模型扩展至更高序数，从而将余归纳类型编码的正确性从W类型推广至涉及有限幂集和有限分布的类型，以及包含存在量化的余归纳谓词。该扩展使得此前在时钟立方类型理论（Clocked Cubical Type Theory）中证明的结果得以在基于集合论的模型中解释，从而验证这些结果在其通常集合论解释下的正确性。