for the few of us.

S-C. Mu, T-C. Tsai, and K. Nakano. XML stream processing using a lazy concurrent language. In Programming Language Techniques for XML (PLAN-X 2008). January 2008.
[PDF]

By chance, I came upon a blog entry by Masahiro Sakai (酒井政裕) in which he, after reading my short comment “Do you know that the S combinator is injective?”, tried to construct the inverse of S and showed that S⁻¹ ○ S = id in, guess what, Agda!