trying to make your type theory 'more convenient' by shoving things into the definitional equality reminds me: a while ago there was a proposal to extend cubical agda with a hierarchy of universes of strict n-types, like arend.
this is a fantastic idea. if you hate yourself. just like strict prop results in something that looks a lot like the ((-1)-connected, (-1)-truncated) factorisation system (a.k.a. (epi, mono)) but mathematically stunted by the necessary inability to prove that a family is strictly (-1)-truncated, an infinite hierarchy of universes of strict n-types results in your type theory being littered with Utter Dogshit versions of the (n-connected, n-truncated) factorisation systems for every n! truly, an incredible development
Amélia Liao 🍊😈
npub105…yvwnw
2026-02-07 13:42:12 UTC
Author Public Key
npub105djthvncz3tms6ke37w4579d0qqmf2e6xt9p7z5h3ayq0wtq7pswyvwnwSeen on
wss://relay.ditto.pubPublished at
2026-02-07 13:42:12 UTCEvent JSON
{
"id": "acddfc1ba8a764bc2e304dfccf3c1a7e9a8fbe33d120eb25c93c82c0fb1c1283",
"pubkey": "7d1b25dd93c0a2bdc356cc7cead3c56bc00da559d19650f854bc7a403dcb0783",
"created_at": 1770471732,
"kind": 1,
"tags": [
[
"proxy",
"https://types.pl/users/amy/statuses/116029635454496685",
"activitypub"
],
[
"client",
"Mostr",
"31990:6be38f8c63df7dbf84db7ec4a6e6fbbd8d19dca3b980efad18585c46f04b26f9:mostr",
"wss://relay.ditto.pub"
]
],
"content": "trying to make your type theory 'more convenient' by shoving things into the definitional equality reminds me: a while ago there was a proposal to extend cubical agda with a hierarchy of universes of strict n-types, like arend.\n\nthis is a fantastic idea. if you hate yourself. just like strict prop results in something that looks a lot like the ((-1)-connected, (-1)-truncated) factorisation system (a.k.a. (epi, mono)) but mathematically stunted by the necessary inability to prove that a family is strictly (-1)-truncated, an infinite hierarchy of universes of strict n-types results in your type theory being littered with Utter Dogshit versions of the (n-connected, n-truncated) factorisation systems for every n! truly, an incredible development",
"sig": "b3a6de8ab98c11cc5dac8859dc7f99cc2919a6e6ff69cffa195218b7272ce7da416e5cef3be77610d2acadcc92cf1e5127bceb6fbf78853c6351356315a0018d"
}