Agda2におけるPropとSet0の違い

Üe🦀 @ranha

@ikegami__ 多分私のは、組込みの力で「便利になった」ようなequalityが欲しいなーっていう言い換えで2例作っただけな気がします。ただSet0とPropの違いは知りたいです！

Ikegami Daisuke @ikegami__

あ、Set0 と Prop の違いはわたしが答えられます : Martin-Loef の型理論では Set0, Set1, Set2, ... : "Proposition as a set" : という概念から、命題は Set0 の型を持つのですが、Set0 と書くと(つづく)

Ikegami Daisuke @ikegami__

命題は Set0 の型を持つのですが、Set0 の使い道は命題だけとは限らないので、命題の型は Prop と、別名をつける規約にしてはどうですか、という話です。Haskell なら type Prop = Set0 です

Üe🦀 @ranha

Agda2で書くと、Prop : Set1 ; Prop = Set0という事ですか...?

Ikegami Daisuke @ikegami__

@ranha ただ、そう書いちゃうと、実装のうえで困ったちゃんなことが起こるので、内部であらかじめ定義しています。将来的には、外部のソルバと連動して動く時などに、Prop しかうけつけてやんねーよ、ばーかばーか（ツン）などの計画を考えているようです

Ikegami Daisuke @ikegami__

困ったちゃんっていうのは、もちろん、モジュールに書くと「隠す」「Prop を別の名前に好きなように定義できる」などのことです

Üe🦀 @ranha

@ikegami__ Propに対しては、風の噂でProof Irrelevanceがあるとかいうのを風の噂くんから聞いた事がある気がするのですが、するとそういう事は無い感じなのですかね?

Ikegami Daisuke @ikegami__

@ranha proof irrelevance ですが、「うーあー」です。慣習にしたがってくれないのと、慣習にしたがったのを混ぜると、ゴミになります

Üe🦀 @ranha

どっちにせよProof IrrelevanceをAgda2でどうやれば良いのかが分からないですし、見た事も無いです・・・。

Ikegami Daisuke @ikegami__

みないことにしましょう

Üe🦀 @ranha

"pragmaOptions :: [OptDescr (Flag CommandLineOptions)]"ココか！！わーここはゆめのらくえんだ！！

Üe🦀 @ranha

あらたに proof-irrelevanceとno-positivity-checkをテニイレタ　タダチニ　ソウビシタマエ

Üe🦀 @ranha

data _==_ {Th : Prop} : Th -> Th -> Prop where refl : (a : Th) -> a == a th2 : {th1 : Prop} (a b : th1) -> a == b th2 a b = refl a コレか！！

Üe🦀 @ranha

でも既に2.2.6さんでは死骸になったぽいですね・・・2.2.4なので動きよる http://wiki.portal.chalmers.se/agda/agda.php?n=Main.Version-2-2-6