The Coq mailing list

[Kristina Sojakova <sojakova.kristina AT gmail.com>]

Dear all,

I am an inexperienced user in Coq and unsure about whether what I am 
trying to do can be even done in it and if so, how. The theory I am 
looking for is the following:

1) I need an impredicative universe, which, however, is *not* 
proof-irrelevant. Let's call it Set.
2) I need to be able to form a \Sigma-type of the form \Sigma x : A. 
f(x) = g(x) : Set. Here A : Set. However, I want the equality type "f(x) 
= g(x)" to be *proof_irrelevant*.

Now I don't know what kind of equality to use. If I use "eq" from the 
Coq standard library then this lands "f(x) = g(x)" in Prop, and that 
is/can be proof-irrelevant, which is good. But of course that doesn't 
work because the whole \Sigma type now lands in Prop too. If on the 
other hand I use some other kind of equality, then it will not be 
proof-irrelevant.

For people who are simultaneously into homotopy type theory, I 
essentially need a propositional truncation of
"f(x) = g(x)" but I don't know how to make it work in the Coq type theory.

Thanks!

Kristina