Home | Notifications | New Note | Local | Federated | Search | Logout
Federated Timeline
🦉@aaa (2026-01-10 04:37:51)
android端末を持っていないからテストできていなかったけどtuskyはavatarが無いと落ちるらしい
でもtokodonとtubaはavatarが無いときユーザー名の頭文字を表示してくれるからabout:blankにするのももったいない気がしてしまう
佐々木@nounashi7298@social.nekokawa.net (2026-01-10 00:57:36)
音楽の歌詞を読まずにメロディしか聴いてない問題、どう受け止めるべきなのか
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-10 00:34:20)
このあと、Listとその長さの依存和とVecが同型であることを示して、同型をパスにして変換できるようにするのをやってみたい
たぶん、Listで定義した非効率で Vec からは定義しにくい rev を Vec から間接的に使えるようになるはず…
たかし@tak4 (2026-01-10 00:17:29)
人を見る時、人の言動はストレスの影響を受けてゐることを前提にしたい。
完全にストレスの無い理想的な状態での言動を想像してみる。特にsnsはストレスのはけ口になりやすいので、そのままの印象で捉へると本人の心の形が分からなくなる。
Reply to @tak4@mstdn.y-zu.org
@risahana@mstdn.jp (2026-01-10 00:04:18)
@tak4 ありー🦋 🦋 🦋
Reply to @risahana@mstdn.jp
たかし@tak4@mstdn.y-zu.org (2026-01-10 00:03:46)
@risahana ハローでっす
@risahana@mstdn.jp (2026-01-10 00:00:12)
ハロー！夜の民＼(^o^)／
たかし@tak4 (2026-01-09 23:58:36)
oepnbsdのデスクトップの背景を真っ黒にしてuiは白ベースだったのも良くなかった。
黒い背景に白いものがあると眼に突き刺さる感じ。
デスクトップの背景を # 808080 にしたら良くなった。xtermの背景も白より少しだけ薄い色にした。
uiを暗くしないのは暗色だと低輝度で見づらいことがあるのと、拘りで色々なものを暗色に統一したくなるから。
コシヌケ1040@ksnk@pawoo.net (2026-01-09 23:35:12)
各国民の自由度はインターネットの自由度で測れるのではないか。と最近考へてみたりする。
Coro@Coro@mstdn.maud.io boosted:
@mattferrell@mastodon.social (2026-01-09 22:17:05)
#FunFactFriday: Attempting to lower diesel use, the Maldives are using floating ocean solar-battery microgrids. Will this become the model for other islands? Source: https://www.pv-magazine.com/2026/01/08/maldives-microgrid-project-with-floating-solar-becomes-model-for-island-renewables-projects/
---Attachments---
https://files.mastodon.social/media_attachments/files/115/865/329/634/713/403/original/70e272ad3cd2c779.jpeg
Matt Ferrell@mattferrell@mastodon.social (2026-01-09 22:17:05)
#FunFactFriday: Attempting to lower diesel use, the Maldives are using floating ocean solar-battery microgrids. Will this become the model for other islands? Source: https://www.pv-magazine.com/2026/01/08/maldives-microgrid-project-with-floating-solar-becomes-model-for-island-renewables-projects/
---Attachments---
https://files.mastodon.social/media_attachments/files/115/865/329/634/713/403/original/70e272ad3cd2c779.jpeg
コシヌケ1040@ksnk@pawoo.net (2026-01-09 22:09:18)
政府にインターネットを遮断されたイラン国民に、イーロンマスクがスターリンクを貸してゐるらしい。人口衛星を持ってゐる富豪はさすが強い。
ところで、万が一アメリカ政府がネットを遮断したとき、スターリンクはどういふ扱ひになるのだらう。スペースXはアメリカの民間企業だよねぇ。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:58:35)
「等しいこと」については「真」か「偽」しかなくて中身がなかった。中身がないから構成する手段もなかった。だから等しさの証明は構成的ではなくて操作的にならざるをえなかった。この問題を解決した Cubical Agda は最強に違いないので色々やってみたいところ。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:44:05)
Agdaだと命題を表現するのに data で型定義をするということがよく行われ、命題の証明は型に対応する証明オブジェクトを構成することによって証明が行うのが自然なアプローチという感じになってる。
しかし、同一性の証明に関しては扱いにギャップがあり sym, cong, subst, rewrite 構文などを使ってうまく命題を操作するプログラムを書く感じになってしまう。
これが Cubical Agda だと、同一性の証明は対応する証明オブジェクト(Path)を構成することになるので、他のアプローチと同じ方法で取り組むことができるのですごい。
コシヌケ1040@ksnk@pawoo.net (2026-01-09 21:42:34)
'00年代にWindows向けの豊かな無償ソフトウェアを幾つも使ってきた所為か、ちょっと画像を縮小するだけのスマホアプリまでことごとく広告有りなのは、なんだかなぁと思ってゐる。
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:35:45)
「同一性」が第一級のオブジェクトじゃなかったという問題が、HoTTによって解決され Cubical Agda では「同一性」を式の操作ではなく「同一性」を表すデータを構成する形で証明できるようになったというところが嬉しさの核であるように思う。
コシヌケ1040@ksnk@pawoo.net (2026-01-09 20:32:20)
ツイッターには、ひとに暴言を吐き捨てるために新しく作られたアカウントがたくさん見受けられるのだけど、俺はそれを「ひよっこチキンアカウント」と呼んでゐる。
Reply to @jns@mstdn.jp
コシヌケ1040@ksnk@pawoo.net (2026-01-09 19:57:29)
@jns あ、死にたがりをばさん登場。
刑部しきみ/InK Mankovitch@jns@mstdn.jp (2026-01-09 19:49:48)
死にたい
コシヌケ1040@ksnk@pawoo.net (2026-01-09 18:06:46)
ぴよぴよぴぴぴ、ひよこがぴょん。
🐤
Reply to @tak4
たかし@tak4 (2026-01-09 16:44:33)
画面を見ない様にして早く寝た。
それによってか眼精疲労が改善した。
先ほどまでは眼の周りの筋が痛かったけど、昨日、筋をこすったのでその反動だらう。今はもう大丈夫!
Coro@Coro@mstdn.maud.io (2026-01-09 12:56:55)
中国、軍民両用品目の輸出規制は日本の「再軍備・核武装を阻止するため」 民生用途に影響なしと説明
https://youtu.be/C4Wl1y9__RI
🦉@aaa (2026-01-09 12:46:23)
日本にサーバーが欲しいけどgmoもさくらもいいイメージがない
諏訪子@suwako@sns.076.moe (2026-01-09 12:37:00)
そっかー
２０２６年「プログラマー」と言えば、「ウェブ開発」しか思い出さないわね・・・
---Attachments---
https://sns.076.moe/media/f60266ec463fce5c7ff45624017b6464b270e6a4ef34feae8ebc365011d78add.png
たかし@tak4 (2026-01-09 11:28:27)
昔のゲーム機にあったbgとスプライトの仕組みは合理的かもしれない
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:47:09)
Agda からrewrite構文と subst が不要になるのは快適すぎる。なんかごちゃごちゃする原因だった。これが Cubical Agda だと lhs と rhs を同時に表す式を書くという考え方になり、これが最強たる所以。これはもう Cubical Agda の前には戻れないかもしれない。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:42:59)
このころだいぶ理解してなかった。Cubical Agdaは等式で式を書き換えようという発想そのものをやめて新しいアプローチに踏み出すやつなので、既存の考え方には全然当てはまらない
https://mastodon.tojo.tokyo/@tojoqk/115862355004663558
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:40:35)
もはや、式を等式で置換するという発想が古いというレベル
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:31:03)
いやまじで Cubical Agda すごいわ。むしろいままでなんでライプニッツの等号で満足していたのかよくわからないレベル。
Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:29:05)
一回 cong 縛りで List の定理を Cubical Agda で色々証明してみて Cubical Agda のパスの感覚を身体的になじませるか
Older Notes