Thanks, will look at both! (I've been interested in HoTT but never looked closer.) Paper looks good, too (for future reference / interested folks, full version available at http://www.ams.org/journals/bull/0000-000-00/S0273-0979-2016... )