Agda の --safe --cubical-compatible への書き換え

割と順調。ZFの書き換えは終わって、圏論の方。まぁ、主に

　functional extentionality

の部分ですね。

　　Extensionality : (a b : Level) → Set _
　　Extensionality a b =
　　　{A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
　　　(∀ x → f x ≡ g x) → f ≡ g

これらは、Free Theorem 排中律と同じで Agda で直接証明できない

あと、

　　≡-irr : { c₂ : Level}　{d : Set c₂ }　{ x y : d } ( eq eq' :　x　≡ y ) → eq ≡ eq'

これは、--with-K としないといけないらしい

仮定にすれば良いので、困るわけではないけど

これに合わせて修正ていくわけですが、見通しが良くなることは確か。全体的には影響しないんですが

　局所的には確かに短くなっているかも

ZF側は外延性の公理の関係だけで、だいたい通ったんですが、圏論の方がちょっと微妙で、全部取れるわけではないらしい

まぁ、でも良い感じかな