Timeline for How many natural operations on subsets are there?
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 28 at 18:49 | history | edited | Martin Brandenburg | CC BY-SA 4.0 |
fix fomatting
|
| Sep 28 at 13:24 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
typo fix
|
| Sep 28 at 13:14 | comment | added | Zhen Lin | Wonderful! I tried playing around with the partial map classifier to see if there is a way to replace automorphisms but quickly realised I have no idea what I'm doing. | |
| Sep 28 at 13:04 | comment | added | Peter LeFanu Lumsdaine | @ZhenLin: I think I have a constructive replacement for that argument, but it’s a bit more fiddly; will edit to add it. | |
| Sep 27 at 14:58 | comment | added | Martin Brandenburg | If $I$ is any set, then operations $P^I \to P$ should also correspond to the deflationary maps $P(I) \to P(I)$, by the same proof. | |
| Sep 27 at 14:52 | comment | added | Martin Brandenburg | Great answer! By the way, for $n=3$ this gives a staggering amount of $4096$ operations. My initial guess was $2^3$ ... ! | |
| Sep 27 at 14:51 | vote | accept | Martin Brandenburg | ||
| Sep 27 at 14:06 | history | edited | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |
emphasised the numerical count (as it answers the title question)
|
| Sep 27 at 12:53 | comment | added | Peter LeFanu Lumsdaine | @ZhenLin: The deflationary property is constructive: for any $U \subseteq X$, $U \in P(X)$ is in the image of $P(U) \to P(X)$, so $\tau_X(U)$ is an image of $\tau_U(U)$ under $P(U) \to P(X)$, so $\tau_X(U) \subseteq U \subseteq X$. I think the non-constructive part can be reduced to one claim: “If $\tau_X(X)$ is inhabited, then it’s $X$.” — assuming this, all the rest of my answer’s argument follows constructively, if phrased carefully-enough. But I’m not sure whether the claim is constructively provable… I can’t see a proof, but I also don’t see that it implies any constructive taboo. | |
| Sep 27 at 12:28 | comment | added | Zhen Lin | Right! I don't even know how to prove that $P (1) \to P (1)$ is deflationary. Naturality says $\bot$ goes to $\bot$ and LEM allows us to conclude the map is deflationary but could we have some funny business away from $\bot$ in general...? | |
| Sep 27 at 12:03 | comment | added | Peter LeFanu Lumsdaine | @ZhenLin: Yes — as far as I can see, it’s using LEM there (and also in the counting, of course). I don”t see a way to do this constructively… would be very interested to know if one can. The difficulty shows up already in the unary case. | |
| Sep 27 at 11:55 | comment | added | Zhen Lin | I suppose "non-intersection" should be "non-empty intersection"? Anyway, inquiring minds want to know: does this require LEM? The part where we permute $U_i$ looks suspect... | |
| Sep 27 at 11:40 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |