Post #1810078
2026-04-30 14:14 UTC
@jonmsterling@mathstodon.xyz If I came up with a rule that is literally written as "∞ < ∞" (I get that maybe there is some additional subtlety it might be abbreviating) and then used it to easily implement coinduction in an intensional dependent type theory, I might take a pause and wonder if something wrong is happening.
Replies (2)
-
@zwarich@hachyderm.io 2026-04-30 14:22
@jonmsterling@mathstodon.xyz
-
@jonmsterling@mathstodon.xyz 2026-04-30 14:15
@zwarich lmaooo One time, a billion years ago, a butterfly flapped its wings and this meant that you were not one of Agda's designers. And here we are...