Plump Ordering

Idea

The plump ordering on a W type is a constructive method of comparing trees based on hereditary domination. It generalizes ordinal comparison to trees that may not be linear, allowing for transfinite induction and bisimulation-like comparisons without LEM.

Definition

Let $W=(\mu X.S◃P)$ be a W type for the container $S◃P$. We define the relations $\le$ and $<:{\mathrm{Rel}}_2(W)$ via an inductive-inductive definition:

$$\begin{array}{rlrl}& \frac{\forall (i:Ps).fi<t}{(s,f)\le t}& & \text{(Bounded by strict predecessors)}\\ & & & \\ & \frac{\exists (i:Ps).t\le fi}{t<(s,f)}& & \text{(Dominated by a predecessor)}\end{array}$$

Properties

1. Reflexivity: can be proven by induction.
2. Mixed Transitivity:
   • $x\le y<z\to x<z$
   • $x<y\le z\to x<z$
3. Well-foundedness: The relation $<$ is well-founded, since it is inductively defined.

Plumpness

A Partial order is Plump if every bounded sub-family has a supremum. For this $W$, the ordering is plump because for any family of trees $(t_i{)}_{i:I}$ bounded by $u$, we can construct a supremum in $W$ (essentially by collecting subtrees).

Relation to Ordinals

• In HoTT, this structure (without set truncated) forms the Brouwer Ordinals.
• If we impose Propositional Truncation (identifying bisimilar trees), we obtain Ordinals.
• Trichotomy ($x<y\vee x=y\vee y<x$) is not provable constructively.