きゅーけー@tojoqk@mastodon.tojo.tokyo: 「同一性」が第一級のオブジェクトじゃなかったという問題が、HoTTによって解決され Cubical Agda では「同一性」を式の操作ではなく「同一性」を表すデータを構成する形で証明できるようになったというところが嬉しさの核であるように思う。

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

Note Detail

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:35:45)
「同一性」が第一級のオブジェクトじゃなかったという問題が、HoTTによって解決され  Cubical Agda では「同一性」を式の操作ではなく「同一性」を表すデータを構成する形で証明できるようになったというところが嬉しさの核であるように思う。


---Replies---

きゅーけー@tojoqk@mastodon.tojo.tokyo (2026-01-09 21:44:05)
Agdaだと命題を表現するのに data で型定義をするということがよく行われ、命題の証明は型に対応する証明オブジェクトを構成することによって証明が行うのが自然なアプローチという感じになってる。
しかし、同一性の証明に関しては扱いにギャップがあり sym, cong, subst, rewrite 構文などを使ってうまく命題を操作するプログラムを書く感じになってしまう。

これが Cubical Agda だと、同一性の証明は対応する証明オブジェクト(Path)を構成することになるので、他のアプローチと同じ方法で取り組むことができるのですごい。