The Coq mailing list

[andré hirschowitz <ah AT unice.fr>]

Hello,

Nice questions. Since experts do not give definite answers, let me bet (not too much!) in favor of consistency! Accordingly,  I urge my  favorite (current) PhD student Anthony to search for a model validating both ProofRelevance and UIP. The rough idea is to take an interpretation where Set and Prop become some universe of sets but this has to be tuned in order to account at least for impredicativity.


ah

2012/12/18 Joseph Tassarotti <tassarotti AT college.harvard.edu>

Hello,

In "Implicit and noncomputational arguments using monads", Letouzey and Spitters define the following type:

Inductive nc (A:Set) : Prop := nc_i : A → nc A.
 
This is used to construct copies of types from Set in Prop. For example, nc nat is a copy of nat that belongs to the sort Prop, so that during extraction terms of this type will be erased. To reason about these terms, they introduce the following axiom, which they call "proof relevance":

Axiom ProofRelevance : ∀(A:Set)(a b:A),
   nc_i a = nc_i b → a = b.

A sketch of an argument is given for why this is consistent with CIC. Of course, it is inconsistent with proof irrelevance. However, is it consistent with UIP? More generally, if I have some type like:

Inductive foo {A1 ... AN B1 ... BM} (x1: A1) ... (xn: AN) : B1 -> ... -> BM -> Prop := ...
 
Would it be safe to combine this ProofRelevance axiom with something like:

Axiom foo_irrelevance: forall A1 ... AN B1 ... BM (x1: A1) ... (xn: AN) (y1: B1) .. (ym: BM)
    (p1 p2: foo x1 ... xn y1 ... ym), p1 = p2.

Thanks!

-Joseph