  Based on Taylor's hereditarily directed plump ordinals, we define the
directed plump ordering on W-types in Martin-L\"of 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.
