きゅーけー@tojoqk@mastodon.tojo.tokyo: 「等しいこと」については「真」か「偽」しかなくて中身がなかった。中身がないから構成する手段もなかった。だから等しさの証明は構成的ではなくて操作的にならざるをえなかった。この問題を解決した Cubical Agda は最強に違いないので色々やってみたいところ。

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

Note Detail

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)を構成することになるので、他のアプローチと同じ方法で取り組むことができるのですごい。
---Reply---
きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:58:35)
「等しいこと」については「真」か「偽」しかなくて中身がなかった。中身がないから構成する手段もなかった。だから等しさの証明は構成的ではなくて操作的にならざるをえなかった。この問題を解決した Cubical Agda は最強に違いないので色々やってみたいところ。