The Coq mailing list

[Burak Ekici <ekcburak AT hotmail.com>]

I seems to me, with a lot of unsure, that your overall point is not 
something doable in CIC?

You could perfectly compile Coq with "impredicative-set" option to make 
Set impredicative (being aware of inconsistencies with some classical 
axioms), build your sigma types (as suggested by Gaetan (item 3rd) and 
Dominique) with equality predicates over them. However, you still want 
your predicate(s) to be proof-irrelevant. Is that easy? The first thing 
came to my mind was adapting "the uniqueness of identity proofs" (<-> 
K-axiom) but then did not seem doable (maybe it is though, did not try). 
You can for sure use standard structural equality of Coq and add one of 
these axioms but now, as you've pointed out, this will fly you back in Prop.

I'd be very happy to know if there exists a way making Kristina's wish 
implementable?

Thanks!

Best,

―

Burak.


On 12/12/2016 09:05 PM, Kristina Sojakova wrote:
> 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
>