I haven’t yet figured out why it’s true under ≃ - I’ll keep trying, but let me know if there’s a quick argument for why this holds. (Default next step for me would be to see if I can restrict attention to the world S1∪S2 then do something similar to my other comment.)
Because S1 and S2 are not a partition of the world here.
EDIT: but what we actually need in the proof is AssumeS1(C)&AssumeS2(C)&⋯≃AssumeS1∪S2(C)&… where the … do result in a partition, so I think this will work out the same as the other comment. I’m still not convinced about biextensional equivalence between the frames without the rest of the product.
UPDATE: I was able to prove AssumeS1(C)&AssumeS2(C)≃AssumeS1∪S2(C) in general whenever S1 and S2 are disjoint and both in Obs(C), with help from Rohin Shah, following the “restrict attention to world S1∪S2” approach I hinted at earlier.
I haven’t yet figured out why it’s true under ≃ - I’ll keep trying, but let me know if there’s a quick argument for why this holds. (Default next step for me would be to see if I can restrict attention to the world S1∪S2 then do something similar to my other comment.)
I am confused, why is it not identical to your other comment?
Because S1 and S2 are not a partition of the world here.
EDIT: but what we actually need in the proof is AssumeS1(C)&AssumeS2(C)&⋯≃AssumeS1∪S2(C)&… where the … do result in a partition, so I think this will work out the same as the other comment. I’m still not convinced about biextensional equivalence between the frames without the rest of the product.
And it seems we do actually need AssumeS1(C)&AssumeS2(C)≃AssumeS1∪S2(C) in the proof to justify:
Without it, we have to show (D1&1R2∪R3)⊗(D2&1R1∪R3)≃AssumeS1∪S2(C)&1R3 instead.
UPDATE: I was able to prove AssumeS1(C)&AssumeS2(C)≃AssumeS1∪S2(C) in general whenever S1 and S2 are disjoint and both in Obs(C), with help from Rohin Shah, following the “restrict attention to world S1∪S2” approach I hinted at earlier.