The Coq mailing list

[Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>]

> But of course that doesn't work because the whole \Sigma type now 
lands in Prop too.

Coq has three different Sigma-like types:

- ex (notation "exists x : A, B") which is implicitly truncated to Prop. 
I think you're using this one when you want one of the others

- sig (notation "{x : A | B}") where the B must be in Prop. You should 
be able to use this one.

- sigT (notation "{x : A & B}"), this one should also work for you.

I don't know why the Coq library doesn't make sig and sigT the same 
type. You can probably pick either as you like.


Another option is to define a custom type for your usage, like this:

    Record foo A B (f g : forall x : A, B x) := { val : A; pr : f val = 
g val }.

It might give you nicer notations but using standard library lemmas 
about sigma types would be harder.

Gaëtan Gilbert

On 13/12/2016 04:05, 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