HoTT: a few more equivs, no longer depends on TypeIsos module
Two: +twist