The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Aleksandar Nanevski wrote:
> Indeed, it's that last case:
>
> forall (A1 A2 B : Type), B -> (A1*B = A2*B) -> (A1=A2)
>
> with equality in Prop, that applies to my problem.
>
> It's amusing that I've ran into univalence just by trying to hack up a 
> bit of meta theory for concurrency. I guess I'll now have to read up 
> on it.

In my experience, the need for a theorem like this more commonly 
indicates that some part of the development should be refactored, rather 
than the need to delve into some new axioms or whatnot.  Could you share 
more of the context?