Cubical Agda の続き

Cubical Agda の論文も読んだんだけど、1011 みたいなバイナリ表記をℕ と≡ で結ぶとかの話が出てくる

そういう方向ですか。そっちの推論自体は要らないかな。割と証明苦労したところだが、それ自体が簡単になるわけではないらしい

でも、それよりも、Cubical Agda と互換にするのが面白いことを発見しました

だいぶ、慣れてきた

　refl で受けるのには条件がある
　パターンの成立しない条件は明示的に消す ( Cubical でないのは書く必要自体がなかった)

あと

　Dec P

が全滅。yes とか no とかで、真偽の理由を取ってこれる(のを自分で作る) 。でも、なんと

　自分で定義すれば回避できる


data Dec (A : Set) : Set where
yes : A → Dec A
no : (A → ⊥) → Dec A

どういうこと?!