The directed plump ordering
Daniel Gratzer, Michael Shulman, Jonathan Sterling
TL;DR
This paper introduces the directed plump ordering on W-types in Martin-Löf type theory, extending Taylor's hereditarily directed plump ordinals with finite joins, enhancing the structural properties of the ordering.
Contribution
It defines a new directed plump ordering on W-types that incorporates non-empty finite joins, expanding the theoretical framework of plump orderings.
Findings
Defines the directed plump ordering on W-types.
Incorporates non-empty finite joins into the ordering.
Extends the properties of the traditional plump ordering.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsHomotopy and Cohomology in Algebraic Topology · Advanced Topology and Set Theory · Algebraic structures and combinatorial models