The Coq mailing list

[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