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

[Robert Harper]

Oh, yes, indeed we were talking about this last week at the IAS: one can consider a bisimulation of packages to be, by univalence, a proof of their equality.  Dan Licata has written about this already, and presented a talk about it at WG2.8 last month.  He and I have been working on this off-and-on for about a year.

Bob

On Dec 5, 2012, at 1:50 PM, Kevin Watkins wrote:

> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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