Is anybody still thinking about Idris and HoTT? https://github.com/fmota/HoTT-Idris/blob/master/README.md I don't see anything more recent than the 2014 discussions.