Home | Notifications | New Note | Local | Federated | Search | Logout

Note Detail


きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:48:01)
Agdaの取り組みに戻れるのが最大の回復といっていい。PLFAの1章をCubical Agdaでやってみようと思っていたところで体調不良で倒れていたので、これをやってみる。
本当は1labをしっかり学習した方がいいような気がするけど、なんというか私は暇なので色々勝手に試行錯誤した方が身につきそうでかつ楽しいので。。。
---Reply--- きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-15 20:49:44) PLFAにでてくる Bin の正規化された構造が自然数と同型な構造のいい具体例なのでちょうどいい。
Reply