Cubical Agda would be so much nicer without happly and funext.


"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

Sign in to participate in the conversation

A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.