agda safe mode

{-# OPTIONS --cubical-compatible --safe #-}

をつけると良いと言われているらしく、せこせこなおしてるんですけどね。

postulate はだめとか、functional-extensionality はだめとか。

それを拒否するわけでもないけど、分離できるならそれがいいかな。

fiso← : (f : R → Bool ) → ffun← ( ffun→ f ) ≡ f

と書きたいわけですが、これだと、functional-extensionality が必要。なので、

ffiso← : (f : R → Bool ) → (x : R) → ffun← ( ffun→ f ) x ≡ f x

こんな風に「関数が等しいのは、すべての要素で値が等しい時」みたいに書き直すらしい。

これでも対角線論法は書けるのか。