[TYPES] a counterexample to Plotkin and Abadi's characterization of equivalence at existential type?

[Kevin Watkins]

A naive question: I wonder if anything has been written on the
homotopy theory of these notions of equality?  Would a homotopical
semantics capture at least part of the syntactic information regarding
"how" two existential packages are equal?

On Wed, Dec 5, 2012 at 12:46 PM, Derek Dreyer <dreyer at mpi-sws.org> wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>> Once again, syntactic reasoning locks in mysteries here.  The remark
>> following Theorem 7 provides the only way in PAL to show that two terms of a
>> an existential type are equal.  So, if you managed to prove that two such
>> terms are equal in PAL, you would have constructed a trasitive composition
>> of simulation arguments.  So, the property you want follows as a metatheorem
>> about PAL.
>
> So how do you show this?  How do you *prove* that simulation is the
> only way to prove that two terms of existential type are equal?  I
> don't see how it follows from Theorem 7.
>
>> That is indeed right.  For closed types, the "only if" direction is trivial.
>> However, for open types, it is not.  You would notice in Theorem 7 the
>> additional condition that x and y have to be related by A[S,rho].  That
>> plays a significant role.
>
> This is fascinating, but I still don't understand concretely what one
> can "do" with the "only if" direction in the case of open types.
>
> Thanks,
> Derek