早起きは三文の得 - Yet Another Ranha

折角なのでtogetterさんを使ってみました。

何か纏める意味はないよなーと思われたものの、幾つかの場所でPropとSet0の違い論争は起こるので他の人がググった時に何か出て来てもしかしたら役に立ってくれるのではないかしらというそういう感じです。

Agda2はConstructiveでありPredicativeでもあるので、CoqのPropと違いそのPropはImpredicativeである事が無いです。

例えばCoqだと

/Users/ranha% rlwrap coqtop
Welcome to Coq 8.2 (February 2009)

Coq < Variable P : Prop -> Prop.
Warning: P is declared as a parameter because it is at a global level
P is assumed

Coq < Check(forall A:Prop,P(A)).
forall A : Prop, P A
     : Prop

Coq < Check(P(forall A:Prop,P(A))).
P (forall A : Prop, P A)
     : Prop

と出来マス。

じゃあAgda2がPropとSet0を分けとるはなんでなんかがずっと不思議だったのですが、Agda2ディレクトリのsrc/full/Agda/Interaction/Options.hsあたりを見ると何か不穏なオプションが一杯あって

pragmaOptions :: [OptDescr (Flag CommandLineOptions)]
pragmaOptions =
    [ Option ['i']  ["include-path"] (ReqArg includeFlag "DIR")
		    "look for imports in DIR"
    , Option ['v']  ["verbose"]	(ReqArg verboseFlag "N")
		    "set verbosity level to N"
    , Option []	    ["show-implicit"] (NoArg showImplicitFlag)
		    "show implicit arguments when printing"
    , Option []	    ["proof-irrelevance"] (NoArg proofIrrelevanceFlag)
		    "enable proof irrelevance (experimental feature)"
    , Option []	    ["allow-unsolved-metas"] (NoArg allowUnsolvedFlag)
		    "allow unsolved meta variables (only needed in batch mode)"
    , Option []	    ["no-positivity-check"] (NoArg noPositivityFlag)
		    "do not warn about not strictly positive data types"
    , Option []	    ["no-termination-check"] (NoArg dontTerminationCheckFlag)
		    "do not warn about possibly nonterminating code"
    , Option []	    ["no-coverage-check"] (NoArg dontCompletenessCheckFlag)
		    "do not warn about possibly incomplete pattern matches"
    , Option []	    ["no-unreachable-check"] (NoArg noUnreachableCheckFlag)
		    "do not warn about unreachable function clauses"
    , Option []	    ["type-in-type"] (NoArg dontUniverseCheckFlag)
		    "ignore universe levels (this makes Agda inconsistent)"
    , Option []     ["sized-types"] (NoArg sizedTypes)
                    "use sized datatypes"
    ]

ほえーという感じです。

このエントリはtogetterさんの捕捉って感じで具体的にどうAgda2でproof irrelevanceぽい事をやるかとかは全部ついったさんで！！！

とにかく早起きは三文の得だと思う事で早起きでモテスリム体型になるのですやりましたギャオン