Strictly Monotone Brouwer Trees for Well Founded Recursion over Multiple Arguments

Ordinals can be used to prove the termination of dependently typed programs. Brouwer trees are a particular ordinal notation that make it very easy to assign sizes to higher order data structures. They extend unary natural numbers with a limit constructor, so a function's size can be the least upper bound of the sizes of values from its image. These can then be used to define well-founded recursion: any recursive calls are allowed so long as they are on values whose sizes are strictly smaller than the current size. Unfortunately, Brouwer trees are not algebraically well-behaved. They can be characterized equationally as a join-semilattice, where the join takes the maximum of two trees. However, this join does not interact well with the successor constructor, so it does not interact properly with the strict ordering used in well-founded recursion. We present Strictly Monotone Brouwer trees (SMB-trees), a refinement of Brouwer trees that are algebraically well-behaved. SMB-trees are built using functions with the same signatures as Brouwer tree constructors, and they satisfy all Brouwer tree inequalities. However, their join operator distributes over the successor, making them suited for well-founded recursion or equational reasoning. This paper teaches how, using dependent pairs and careful definitions, an ill-behaved definition can be turned into a well-behaved one. Our approach is axiomatically lightweight: it does not rely on Axiom K, univalence, quotient types, or Higher Inductive Types. We implement a recursively-defined maximum operator for Brouwer trees that matches on successors and handles them specifically. Then, we define SMBtrees as the subset of Brouwer trees for which the recursive maximum computes a least upper bound. Finally, we show that every Brouwer tree can be transformed into a corresponding SMB-tree by infinitely joining it with itself. All definitions and theorems are implemented in Agda.