The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le samedi 30 avril 2011 à 13:21 +0200, 
ericfinster AT gmail.com
 a écrit :
> Hi!
> 
> I'm very new to Coq, so I hope my question will not sound to silly to 
> everyone.
>  I'm a homotopy theorist by training, and I've become interested in this new
> interpretation of Leibniz equality as "paths" in homotopy theory.  I've been
> trying to prove some simple things about dependent sums (which are 
> fibrations
> to a homotopy theorist), and I'm having some difficulty which I was hoping
> someone might explain.        
> 
> So here is the notation I'm using for equality
> 
>   Inductive paths {A} : A -> A -> Type := idpath : forall x, paths x x.
>   Notation "x ~~> y" := (paths x y) (at level 70).
> 
> Now what's bugging me is that projections from dependent sums only seem to
> respect this equality in one direction.  For example, the following fails
> 
>   ** Fails **
>   Lemma test (X : Type) (P : X -> Type) (a : { x:X & P x }) :
>     existT (fun x : X, P x) (projT1 a) (projT2 a) ~~> a.
>   Proof.
>     apply idpath.
>   Qed.

It's just that "existT ... (projT1 a) (projT2 a)" is not convertible to
"a" unless "a" is itself of the form "existT ... x y". Just make it so:

  destruct a.
  apply idpath.

Best regards,

Guillaume