Meanwhile, I chose to add ‘bot and ‘top, and to bound the lists at both ends, because these ordered lists are but one instance of a general scheme for constructing ordered data structures. It’s certainly possible to define ordered cons-lists with only a lower bound, but binary search trees require both bounds.

The grammar F ::= 1 | F+F | F[]F | rec determines a class of functors whose fixpoints are readily orderable, given some notion of element X with order < =

[[_]] : F -> (X -> X -> Set) -> (X -> X -> Set)
[[ 1 ]] R l u = :- l <= u
[[ F + F' ]] R l u = [[ F ]] R l u + [[ F' ]] R l u
[[ F [] F’ ]] R l u = (x : X) * [[ F ]] R l x * [[ F' ]] R x u
[[ Rec ]] R l u = R l u

The idea is that everywhere there’s a pair, there’s a pivot. Ordered lists are given by the code 1 + (1 [] Rec). Binary search trees are given by the code 1 + (Rec [] Rec).

Also, wouldn’t it be enough to just extend the naturals with ‘bot and just always let the upper bound in OList be infinity?