きゅーけー@tojoqk@mastodon.tojo.tokyo: あー、hcomp のところまで来て自分が Cubical Agda に抱いていたメンタルモデルがかなり間違っていることに気づいた。これパスでつなげるイメージを抱いたから線路的な的なもの組む感じになるのかと思ったけど全然そうじゃなくて高次立方体を構成していくことで等式の連鎖を実現する感じなのか

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

Note Detail

Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-06 22:51:37)
等式に方向があるのはACL2のメリットだと前から思ってはいたんだよなあ
---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-08 01:25:09)
あー、hcomp のところまで来て自分が Cubical Agda に抱いていたメンタルモデルがかなり間違っていることに気づいた。これパスでつなげるイメージを抱いたから線路的な的なもの組む感じになるのかと思ったけど全然そうじゃなくて高次立方体を構成していくことで等式の連鎖を実現する感じなのか


---Replies---

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:42:59)
このころだいぶ理解してなかった。Cubical Agdaは等式で式を書き換えようという発想そのものをやめて新しいアプローチに踏み出すやつなので、既存の考え方には全然当てはまらない
https://mastodon.tojo.tokyo/@tojoqk/115862355004663558