The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

I do not know if that might be of some help to you but
for Prop types P : A -> Prop (like e.q. identity types),
the two types (exists x, P x) and { x | P x } are
interchangeable. Indeed, one can prove

Definition ex_rect (A : Prop) (P : A -> Prop) (Q : Type) : (forall x :
A, P x -> Q) -> (exists x, P x) -> Q.
Proof.
  intros HA H.
  assert ({ x | P x}) as H1.
    destruct H as (x & ?); exists x; assumption.
  destruct H1 as (? & H1); revert H1; apply HA.
Qed.

Hence you can destruct (exists u,f u = g u) in a Type context
by replacing it with { u | f u = g u }.

Best,

Dominique

----------------------------------

Le 13/12/2016 à 10:31, Gaetan Gilbert a écrit :
>> 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
>>
>