Suppose I assume the existence of a countable sequence of types A₀, A₁, A₂, … such that A₀ = ΣA₁, A₁ = ΣA₂, etc., a tower of suspensions going down.
| 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]
If it's possible for A₀ to not be trivial, then I have a hunch it ought to behave kind of like a "negative point"; I think for any function B → C I can naturally construct a map from a colimit of C many copies of A₀ to B many copies of A₀.
Is A₀ necessarily contractible? Be careful not to think I'm asking a very similar-sounding but distinct question: I know if the sequence was ordered the other way around, with A₀ = 0, A₁ = ΣA₀, A₂ = ΣA₁, etc. then the colimit of the sequence ("the infinite-dimensional sphere") would be contractible.
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.
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
🐈🐈🐟🐟🐟
🐈🐈🐈🐈🐈
Ugh, I got lovely light-weight notifications working via either mobile firefox or chrome with https://github.com/jcreedcmu/notifier/ but then it seems like both firefox and chrome have made it impossible to have these notifications cause vibration. Which was exactly what I wanted to make it possible for things happening on the desktop to actually let me know asynchronously when I step away from the computer...
@edwinb Somewhere buried in here was the idea that traversal of a term while it is being initially typechecked would match very closely the traversal of the same term "executing" as the typechecker for its own arguments