The two types of irrelevance: irrelevance à la parametricity, or "I promise I won't look at it", and irrelevance à la Prop (ZSTs for Rustaceans), or "go ahead, there's nothing to see".
What's their relationship? Some duality?
Conversation
Something something multiplicity 0. I think there is mumbling from Mcbride about Prop being abit hacky, but I don't know about what the solution is. Could you also have things that are irrelevant because they exist in a later execution phase? Or would that just be ill-formed. 🤔
1
My hunch would be that multiplicity 0 is closely related to the "irrelevance à la parametricity" half of things, whereas "à la Prop" is the sort of thing which can be erased *even if you have infinitely many of them*. Could be mistaken though!
1
(The second half of your tweet reminds me of McBride's "oil and water" remark here: pigworker.wordpress.com/2014/12/31/wor. Is that what you had in mind? N.B. it's been a while since I read (or tried to read) that and I can't remember how much of it I got.)
2
1
If you have not studied Kripke semantics (more for intuitionistic logic than for modal logic), consider it a prerequisite study. I feel you probably want to prove yourself that what holds in a world holds in later worlds as well, but that might be personal bias.
1
2
Yes, "find out what this Kripke stuff is about" has been on the backburner for years. If you happen to know of a good blog-post-length introduction (or set of slides; anything but a book), would appreciate... :)
1
2
The basic reference I use is en.m.wikipedia.org/wiki/Kripke_se. But I confess I have cheated by studying an instance for ages...
1
1
Thanks a bunch! Resisting the urge to curl up in a corner in despair! Will persist though!
That urge is not the correct reaction. Took me two years to get this properly, and I had to because it shows up in my PhD thesis in step-indexing. As usual, I got the proofs by failing them. But first, examples!
1
(But examples on Twitter are dangerous because how do I check what I can assume? Sorry, forging ahead).
2
1
Show replies