Yes I think you hit it on the nail. My logic depended on the aggregator being a recursive monoid, with: 1) Special handling for a unit list, where the unitary

Yes I think you hit it on the nail. My logic depended on the aggregator being a recursive monoid, with: 1) Special handling for a unit list, where the unitary element is returned, and 2) Special handling for an empty list, where the identity element of the monoid is returned OR we get explicit that the case of the empty list is simply already it’s simplest form, and we choose to define that equivalent to the monoid’s identity So i skipped a step by “finding” the identity from the aggregator’s behavior, instead of directly from the monoid it is based on. —— Alternatively, I am liking the idea of defining this list vs pair, aggregator vs monoid relations more tightly. Empty braces unify the syntax for “zero” with the semantics “nothing” between the braces. How else can you join those semantics and syntax? Likewise, starting with unary natural numbers, syntactically and semantically, a list of 1’s is the number. So which comes first? A unary monoid addition of 2 lists of ones (n-way concatenations of unitary 1), or an n-way sum-concatenation that each unary number actually consists of? I think they are more tightly bound definitions than our typical syntax suggests, when we get down to the semantics = syntax level.