有向丰满排序
The directed plump ordering
摘要：
基于Taylor的遗传有向丰满序数，定义了Martin-Löf类型论中W-型上的有向丰满序.这种排序类似于丰满排序，但除了丰满排序的通常属性之外，还配备了非空有限连接。
英文摘要：
Based on Taylor's hereditarily directed plump ordinals, we define the directed plump ordering on W-types in Martin-Löf type theory. This ordering is similar to the plump ordering but comes equipped with non-empty finite joins in addition to the usual properties of the plump ordering.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
