[ 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
