The Coq mailing list

[Aleksandar Nanevski <aleks.nanevski AT imdea.org>]

On 8/5/12 7:07 PM, Adam Chlipala wrote:
> 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?

Thanks Adam. Indeed, you are right, and I have in fact refactored my 
development in this case (it would be a bit too long to explain the 
details now). I was just curious whether it was *necessary*.

 Best,
Aleks