I posted a version written in Idris here 
(https://github.com/jdolson/univalence-from-scratch) if anyone is curious. 
-Jeff