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

Note Detail

Reply to @tojoqk@mastodon.tojo.tokyo
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:29:05)
一回 cong 縛りで List の定理を Cubical Agda で色々証明してみて Cubical Agda のパスの感覚を身体的になじませるか

---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:31:03)
いやまじで Cubical Agda すごいわ。むしろいままでなんでライプニッツの等号で満足していたのかよくわからないレベル。
Reply 
---Replies---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 09:40:35)
もはや、式を等式で置換するという発想が古いというレベル