Cubical Agda would be so much nicer without happly and funext.
Follow
"Oh, I'll use representability so I can work with the category of Sets wont that be nice"
Meanwhile happly is sitting around the corner just waiting to bonk me with the "all your arguments are in the wrong order" hammer
