I'm a little confused about how to do this in a way such that the two constructions are strictly inverses of each other (as per 5c). In particular, when I go from the carrier type of the list, X, to the set for the monoid, I had to modify it to be 1 + X instead of X. Because how else am I going to guarantee that my monoid set has a unit in it?

(I assume that the function associated with the list algebra uses identity on the carrier type when the second parameter is the empty list.)