rntzJun 25
the right notion of equality on existential types should be something like bisimulation, right? is there a standard reference for this?
Show threadJon SterlingJun 25

@rntz There are parametricity models where some kind of bisimulation is the relational interpretation of the existential type…

But my take is that this is a distinct question from what the “right notion of equality” is.

Show threadrntz

my unsophisticated intuition is that the type of (not-necessarily-finite) state machines over an alphabet a ought to be: (exists s. s * (s -> bool) * (s * a -> s)). so somehow equality on existentials should capture bisimulation of state machines. which parametricity models are you thinking of - do they agree with this?

I'm also interested in why this might not be the "right" notion of equality - but for what I'm doing right now it's the notion of equality I care about :P.

Jun 25 at 6:40amWeb
Show threadOwen LynchJun 25

@rntz The way to think about this is, first of all, to clarify what the existential is doing here. Is it serving in for a sigma type over some universe of types? In that case, the question is what are identifications between types. If we are working univalently, then these are isomorphisms, but if we are working in something like narya, these might be relations.

But if the existential is meant to quotient in some way, then that's a different story. I'm not totally sure what would happen here; perhaps it would just produce the set of states in the terminal coalgebra, in which case equality is bisimulation.

Show threadJon SterlingJun 25

@olynch @rntz Just to add to this discussion:

1. I agree that if it is really standing for an honest sigma type, it reduces to identifications of types and dependent pairs.

2. I would say that the relational interpretation (e.g. in Narya, but also in general) is not giving an explanation of equality because equality == satisfying something along the lines of the J-rule. Instead, the relational stuff in Narya would be describing a kind of additional path-like structure that could be distinct from equality.

3. Existentials are the abstract rules for what happens when you restrict a sigma type into a reflective subuniverse. So the actual equational theory of the existential completely depends on what this subuniverse is, and so there is no real answer to the question, "What is the 'right' notion of equality on existentials?". It really depends on what, precisely, is making the sum into a weak sum.

There *is* a definitive answer to "When should to functions out of the existential be equal", but as far as looking at maps in, this is going to depend on the totality of everything else that is included.