This isn’t true, because ∙1 doesn’t just ignore b1 here (since r∈R1). I think the route is to say “Let h(b′2)=f2 . Then ∙1 must treat f1 and f2 identically, meaning that either they are equal, or the frame is biextensionally equivalent to one where they are equal.”
Using the idea we talked about offline, I was able to fix the proof—thanks Rohin! Summary of the fix: When D1 and D2 are defined, additionally assume they are biextensional (take their biextensional collapse), which is fine since we are trying to prove a biextensional equivalence. (By the way this is why we can’t take b1=b2, since we might have A⊇B1≠B2⊆A after biextensional collapse.) Then to prove h=hf1, observe that for all b∈B1, b∙1h(b′2)=b∙1h(b2) which means b⋆1h(b′2)=b⋆1f1, hence h(b′2)=f1 since a biextensional frame has no duplicate columns.
How is this supposed to work (focusing on the h=hf1 claim specifically)?
h(b′2)=b1∙1h(b′2)=r.Earlier, hf1 was defined as follows:
but there is no reason to suppose f1=r above.
The problem is a bit earlier actually:
This isn’t true, because ∙1 doesn’t just ignore b1 here (since r∈R1). I think the route is to say “Let h(b′2)=f2 . Then ∙1 must treat f1 and f2 identically, meaning that either they are equal, or the frame is biextensionally equivalent to one where they are equal.”
Using the idea we talked about offline, I was able to fix the proof—thanks Rohin!
Summary of the fix:
When D1 and D2 are defined, additionally assume they are biextensional (take their biextensional collapse), which is fine since we are trying to prove a biextensional equivalence. (By the way this is why we can’t take b1=b2, since we might have A⊇B1≠B2⊆A after biextensional collapse.) Then to prove h=hf1, observe that for all b∈B1, b∙1h(b′2)=b∙1h(b2) which means b⋆1h(b′2)=b⋆1f1, hence h(b′2)=f1 since a biextensional frame has no duplicate columns.