You said in words that
Every S can be reconstructed from a sequence of updates:
but your formula
forall s. exists [a]. s == foldl update empty [a]
says that a (not necessarily unique) sequence of updates can be reconstructed from every S. I think you meant something like "there are no elements of S but those that can be constructed by a sequence of updates". I'm a little confused by "a" being lower case. There's a little wrinkle that tells me this isn't going to be simple. type A = Bool newtype S = S [A] empty :: S empty = S [] update :: S -> A -> S update o@(S (x:xs)) y | x == y = o update (S xs) y = S (y:xs) reconstruct :: S -> [A] reconstruct (S xs) = xs Here update is *locally* idempotent: update (update s a) a == update s a But it's not *globally* idempotent: you can build up a list of any desired length, such as S [False,True,False,True,False], as long as the elements alternate. Perhaps I have misunderstood your specification.