Computing with Univalence - Daniel Licata