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