To see that some restriction is required here (not imposed by HOL), consider that if Chu(w) may contain arbitrary Cartesian frames over w then we would have an injection 2Chu(w)→Chu(w) that, for example, encodes a set S⊆Chu(w) as the Cartesian frame CS with Agent(CS)=S (the environment and evaluation function are unimportant), which runs afoul of Cantor’s theorem regarding the cardinality of Chu(w).
I wouldn’t be surprised if a similar encoding/injection could be made using just the operations used to construct Cartesian frames that appear in this sequence—though I have not found one explicitly myself yet.
To see that some restriction is required here (not imposed by HOL), consider that if Chu(w) may contain arbitrary Cartesian frames over w then we would have an injection 2Chu(w)→Chu(w) that, for example, encodes a set S⊆Chu(w) as the Cartesian frame CS with Agent(CS)=S (the environment and evaluation function are unimportant), which runs afoul of Cantor’s theorem regarding the cardinality of Chu(w).
I wouldn’t be surprised if a similar encoding/injection could be made using just the operations used to construct Cartesian frames that appear in this sequence—though I have not found one explicitly myself yet.