good times with the online pictionary with friends
| foundations | constructive, univalent |
| gh | https://github.com/jcreedcmu |
@jcreed
- 563 Followers
- 229 Following
- 4.5K Posts
theorems, types, tunes, typefaces, terms-of-art, tropes, technicalities. [en/eo, +ε es/zh/fr/pl/jp]
@cdrichards trogdor was definitely one of the earlier guesses
@hallasurvivor (I'm in no way disagreeing with you that this is funny :)
@hallasurvivor walking from here to there (points to easily visible location) is straightforward. walking from here to here (shifts weight to other foot) is trivial.
ok, I managed to make a minimal native android app with 'capacitor', which is apparently the spiritual descendant of 'cordova'. Reminds me how much pain java development always seems to entail. Nonetheless it works and I can get vibration on notifications, even.
@jdw I'm using "merely* in the HoTT sense of truncatons ~= proof irrelevance... my natural tendency at this point in my evolution as a mathematician is to treat "forall" and "exist" as always meaning pi and sigma, and "merely exist" is a sigma wrapped with a propositional truncation
@jdw Let's say your proposition is
A = "for any v : R^2, there exist suitable r, u such that v = r * u"
and a variation of that is
A' = "for any v : R^2, there *merely* exist suitable r, u such that v = r * u"
My current belief is that:
A doesn't imply falsehood
A implies something decisively anticonstructive, i.e. the existence of a total discontinuous function R -> R
it does not yet seem obvious to me that A' necessarily implies anything decisively anticonstructive the way A does
@jdw The R -> R function I have in mind is, simply: given any x : R, consider the vector (x, 0). Use your proposition to extract its normalization u = (ux, uy). Return ux.
@jdw I think not, although I'm not 100% confident that it might not depend in some fiddly way on how you constructively define the reals.
My intuition is this: if your proposition were true, you could define a total function R -> R which is -1 below 0, and +1 above zero. This should be discontinuous regardless of the value at zero, and constructively we shouldn't be able to make a total discontinuous function R -> R.
whoops, this was meant to be a link to https://hci.social/@chrisamaphone/116307319860900149
fun little trivia game, I got
catfishing.net
#643 - 7/10
🐈🐈🐟🐟🐟
🐈🐈🐈🐈🐈