Selective applicative functors formalised in Agda. Take a look at he Haskell implementation, and Andrey Mokhov's blog post. This is work in progress.