Observational Equality

[jonsterling]

• [x] proof irrelevance (either via Prop or squash type); this is crucial, since I do not think that the system has canonicity without it
• [x] add refl
• [x] add coe
• [x] add coh

[ghost]

Nice! Very interested to see how this turns out. The code looks really clean too.

[jonsterling]

Thanks!

One thing I'm not certain about is whether I am doing checking & NBE for the equality type correctly. To summarize, for an equality prop Eq(A;B;M;N), I compute a type of proofs equal(A;B;M;N) (which is the book equality at the types A,B). Then I have a rule like

p <= equal(A;B;M;N)
------------------------
p <= Eq(A;B;M;N)

Of course, this is better than having the Eq operator compute to a type, since we wouldn't otherwise be able to recover the fact that we have an equality proof. But this feels a little strange, and I wonder if I am doing something wrong; in particular, I wonder if there is extra stuff I need to throw into the NBE to make this be well-behaved; my intuition is that I should add eta expansions at Eq, for instance.

[jonsterling]

(It's worth noting that Conor uses a separate prop universe for this, and that might at least simplify some of these questions. But I find a prop universe to be pretty distasteful, and I wonder if I can get away with not doing it.)

[ghost]

Hmm, honestly I'm not sure. I'll have to take a closer look and maybe compare with Conor's work. Eta-expansion at Eq sounds plausible though. I suppose you'd find out one way or another if you intend to prove correctness of the NBE although that's a real hassle to do formally even for the STLC…

[jonsterling]

By the way, I'm rethinking my decision to leave Eq as a non-computed constant with special cased rules. I think that the problems I noted might disappear as soon as I have learnt to think a little more clearly about the structure that we are dealing with (canonical vs neutral terms, analytic vs synthetic judgement, etc.). I'm going to just leave this for a few days probably while I think it over and re-read the OTT literature.

[jonsterling]

So I ended up doing this without a separate prop universe, since I have always found that distasteful (it has its advantages, but I really want to see how far I can get without it). Instead, I just built in a squash type; terms of squash types are ensured to be boxed by means of eta expansion.

[jonsterling]

I think that whilst this will almost certainly continue to receive refinement over time, it is good enough to work with now.

[ghost]

So I ended up doing this without a separate prop universe, since I have always found that distasteful (it has its advantages, but I really want to see how far I can get without it). Instead, I just built in a squash type; terms of squash types are ensured to be boxed by means of eta expansion.

Very interesting! I like this idea since I also found the prop universe approach somewhat distasteful…

[jonsterling]

One very surprising thing that occurred is that somehow the NBE is eta expanding closed Refl terms into canonical proofs! I do not really know how this happened, but it's kind of neat. Makes me wonder, though, if the NBE as I've implemented it has subject reduction, since I recall that it was not possible to "prove" reflexivity in general for obs-eq...

[ghost]

Hmm, so that's what you meant with the comment. That's pretty interesting. I'm not sure what it means for subject reduction. Probably worth double checking the implementation although I do recall that in one of the variants of OTT I implemented in Agda that also didn't use prop (and had heterogeneous equality as a derived notion), I was able to prove some stuff about equality that apparently wasn't supposed to work either…

[jonsterling]

Yes, I think a double-check of the implementation is definitely a good idea.

Btw, that's interesting that you'd used homogeneous equality at the bottom; any advice there? (i.e. is it a good idea?). Also, do you recall what you did to maintain canonicity in the absence of prop (curious if you did what I did, or something else)?

[ghost]

Btw, that's interesting that you'd done used homogeneous equality at the bottom; any advice there? (i.e. is it a good idea?). Also, do you recall what you did to maintain canonicity in the absence of prop (curious if you did what I did, or something else)?

Unfortunately I don't recall the specifics. That was shortly before Chris Kapulkin and Peter Lumsdaine visited and then I got caught up wasting time trying to do higher-dimensional CWFs… I don't think I finished the OTT stuff and there were still issues I was trying to work out with some proofs. I'll see if I can dig something up from my archives. I think what you're doing here is probably much more sophisticated though.

I do remember that homogeneous equality made more sense to me since I was trying to understand things from the categorical side and it worked out nicely with families of setoids whereas heterogeneous equality didn't. At the time, when I had talked to Thorsten and Conor about it, I didn't get the impression that there was a good theoretical justification for using heterogeneous equality even though it made some sense from a usability perspective. I didn't get far enough to determine if it was a good idea beyond that.

[jonsterling]

Gotcha. Heh, just realized that the Box stuff in here is totally wrong... I'll rewrite that tomorrow.