The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 03/06/2013 15:01, Pierre-Marie Pédrot wrote:
> Your lemma implies in particular proof-irrelevance (take A to be unit
> and the predicate to be any proposition), so no.

And actually it is strictly equivalent (proof attached), without even
requiring to derive injectivity of dependent pairs through the
particular case of proof-irrelevance that is UIP.

PMP
Module Type P.

Axiom sig_map_eq : forall
  {A   : Type}
  (P   : A -> Prop)
  (x y : sig P),
  proj1_sig x = proj1_sig y -> x = y.

Lemma PI : forall (P : Prop) (p q : P), p = q.
Proof.
intros P p q.
pose (u := existT (fun (_ : unit) => P) tt p).
pose (v := existT (fun (_ : unit) => P) tt q).
change p with (proj2_sig u).
change q with (proj2_sig v).
rewrite (sig_map_eq _ u v); [reflexivity|reflexivity].
Qed.

End P.

Module Type Q.

Axiom PI : forall (P : Prop) (p q : P), p = q.

Lemma sig_map_eq : forall
  {A   : Type}
  (P   : A -> Prop)
  (x y : sig P),
  proj1_sig x = proj1_sig y -> x = y.
Proof.
intros A P [u p] [v q] Hrw; simpl in Hrw.
destruct Hrw; f_equal.
apply PI.
Qed.

End Q.

Attachment: signature.asc
Description: OpenPGP digital signature