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.