PhD Meeting 20251127

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.

Link to original

Circular transclusion detected: Plump-Order

Stratified induction: $P:T^{\ast }\Rightarrow \mathrm{Set}$ $Pt=\{u:T.u<t\}$

$FX:=1+\mathbb{N}\to X$

Can we define every inductive type as a colimit?

QIT can’t be modeled in ZF without choice. Mobile trees (1 + N→X) + permutaiton invariant.