The directed plump ordering
Logic in Computer Science
2022-03-21 v2 Logic
Abstract
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.
Cite
@article{arxiv.2202.07329,
title = {The directed plump ordering},
author = {Daniel Gratzer and Michael Shulman and Jonathan Sterling},
journal= {arXiv preprint arXiv:2202.07329},
year = {2022}
}
Comments
Added funding acknowledgment