[Agda] Proof irrelevance and self-realizing formulas

[Shin-Cheng Mu]

Hi,

I've been eavesdropping this interesting discussion for 2 days,
while building up courage to interrupt and ask novice questions
again... :)

Is what I say below correct?

There are now at least 3 interpretations of "proof irrelevance"
I have heard of:

1. The CC/Coq approach. Prop is impredicative and therefore,
    in any set theoretic model, Prop could have only one
    member -- *.

    Therefore not only proofs of equal propositions are equal,
    but all proofs are equal. Some work went to length
    (e.g. [1]) talking about unifying (\x -> *) and *.

    I think it is under this interpretation that I can
    prove the law of excluded middle [2], is it?
    (If I take equality on propositions to be "if and only if".)

2. The Conor/Thorsten/OTT approach. Prop is embedded into Set
    in the usual way -- Sigma for conjunction, Pi for implication, etc.
    Proofs of the same proposition are equal, but not all proofs are *.

    Is it only in this interpretation that we'd better not have
    disjunction in Prop, to avoid having two proofs of P \/ P?

3. Prop and Set live in separate spaces, mainly to distinguish
    computationally interesting parts from uninteresting parts
    of a program/proof. Quoting Andrej:

      "Anything that can be computed using a proof p : P, can also be
       computed without it."

    Is this interpretation mostly correlated with 1.?

sincerely,
Shin

[1] A. Miquel and B. Werner. The not so simple proof-irrelevant
     model of CC.
[2] A blog post of mine
        http://www.iis.sinica.edu.tw/~scm/?p=133
     with information assembled from various places...