But then shouldn’t there be a natural biextensional equivalence C→^C?
Suppose C=(A,E,⋆), and denote ^C=(^A,^E,⋆).
Then the map A→^A is clear enough, it’s simply the quotient map.
But there’s not a unique map ^E→E - any section of the quotient map will do, and it doesn’t seem we can make this choice naturally.

I think maybe the subcategory of just “agent-extensional” frames is reflective, and then the subcategory of “environment-extensional” frames is coreflective.
And there’s a canonical (i.e natural) zig-zag C→(^A,E,⋆)←^C

But then shouldn’t there be a natural biextensional equivalence C→^C? Suppose C=(A,E,⋆), and denote ^C=(^A,^E,⋆). Then the map A→^A is clear enough, it’s simply the quotient map. But there’s not a unique map ^E→E - any section of the quotient map will do, and it doesn’t seem we can make this choice naturally.

I think maybe the subcategory of just “agent-extensional” frames is reflective, and then the subcategory of “environment-extensional” frames is

coreflective. And there’s a canonical (i.e natural) zig-zag C→(^A,E,⋆)←^CYou might be right, I am not sure.

It looks to me like it satisfies the definition on wikipedia, which does not require that the morphism rB is unique, only that it exists.