  Ordinals can help prove termination for 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 natural numbers with a limit
constructor, so a function's size can be the supremum 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, it
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. We show
how, using dependent pairs and careful definitions, an ill-behaved definition
can be turned into a well-behaved one, with light axiomatic requirements. We
implement a recursively-defined maximum operator for Brouwer trees that matches
on successors and handles them specifically. Then, we define SMB-trees 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 joining it with itself an infinite number of times.
All definitions and theorems are implemented in Agda.
