The Coq mailing list

[ericfinster AT gmail.com]

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.

While the next two are okay:

  Lemma test2 (X : Type) (P : X -> Type) (x : X) (u : P x) :
    projT1 (existT (fun x:X, P x) x u) ~~> x.
  Proof.
    apply idpath.
  Qed.

  Lemma test3 (X : Type) (P : X -> Type) (x : X) (u : P x) :
    projT2 (existT (fun x:X, P x) x u) ~~> u.
  Proof.
    apply idpath.
  Qed.

Could someone explain to me what's going on (maybe something to do with eta?),
and possibly if there are common tricks for dealing with this kind of thing?

Thanks very much!

Eric Finster