论文标题
定向的丰满订购
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.
