Worked out the blog post http://homotopytypetheory.org/2012/01/22/univalence-versus-extraction/ in Coq.