Some notes on plump ordinals

In this exposition, we attempt to formalise a treatment of Paul Taylor’s notion of plump ordinals in weak intuitionistic axiomatic set theories such as IKP. We will explore basic properties of plump ordinals, especially in relation to Gödel’s constructible universe $L$ and incomparable codings. As a quick application, we explain at the end how plump ordinals can be used to build a Heyting-valued model $V^{\mathbb{H}}$ from a classical $V\models \mathrm{Z}\mathrm{F}\mathrm{C}$ such that for some arbitrary, fixed $x\in V$ we have $V^{\mathbb{H}}\models \mathcal{P}\left(\check{x}\right)\in L$.